[opentheory-users] Version 6 of the OpenTheory article file format standard

[Joe Leslie-Hurd]

Hi Michael,

You're quite correct: the writing is a little sloppy in the
implementation-dependent section of the standard.

Cheers,

Joe

On Mon, Dec 1, 2014 at 3:39 PM, Michael Norrish
<michael.norrish at nicta.com.au> wrote:
> The pragma operation says that it can only accept an object on the top of the
> stack of the form "debug".  Presumably, that's really an object of the form
> Name([], "debug"), as would be generated by having that string be the previous
> command in the file.
>
> Michael
>
> On 02/12/14 10:32, Joe Leslie-Hurd wrote:
>> I'm pleased to announce a new version of the OpenTheory article file
>> format standard, used for encoding theories of higher order logic. The
>> new version of the article standard is version 6, and is available at
>>
>> http://www.gilith.com/research/opentheory/article-6.html
>>
>> I would like to thank Rob Arthan, Mario Carneiro, Ramana Kumar and the
>> others who have contributed to defining version 6 of the article
>> standard: this is a concrete step towards the goal of sharing theories
>> between the HOL family of theorem provers.
>>
>> Cheers,
>>
>> Joe
>>
>> *** Summary of changes in version 6 of the article file format standard
>>
>> 1. The new command version allows a writer to specify the version of
>> the OpenTheory article format used in an article so that a reader can
>> take appropriate action.
>>
>> 2. The new command pragma allows a writer to ask for a reader to take
>> some implementation-dependent action, e.g., to produce debug output.
>>
>> 3. The new commands proveHyp, sym and trans provide an efficient
>> implementation of three frequently used derived inference rules
>> allowing writers to produce more compact article files.
>>
>> 4. The new command defineConstList provides a more abstract principle
>> for constant definition. This supports recent extensions to HOL4 and
>> ProofPower.
>>
>> 5. The new command hdTl provides a destructor function for lists (an
>> inverse to the existing cons command). This enables writers to store
>> constants introduced by the new command defineConstList in the
>> dictionary.
>>
>> 6. The command defineTypeOp has been changed so that the theorems
>> giving the defining properties of the abstraction and representation
>> functions have no free variables.
>>
>> 7. There have been minor clarifications to the description of the
>> primitive types processed by the virtual machine.
>>
>> 8. A note has been added to clarify the description of the command
>> deductAntisym.
>>
>> The changes between version 5 and version 6 of the article file format
>> standard are highlighted at
>>
>> http://www.gilith.com/research/opentheory/article-5-6.html
>>
>> *** Converting between version 5 and version 6 articles
>>
>> The latest release of the opentheory tool, which is available at
>>
>> http://www.gilith.com/software/opentheory/
>>
>> supports a new --output-version parameter to select the version of
>> articles that it outputs, like so:
>>
>> opentheory info --article -o output5.art --output-version 5 input.art
>> opentheory info --article -o output6.art --output-version 6 input.art
>>
>> In this example the input article input.art can be either version 5 or
>> version 6.
>>
>> The latest release of the OpenTheory standard theory library uses
>> version 6 articles:
>>
>> http://opentheory.gilith.com/?pkg=base
>>
>> To install the standard theory library using the opentheory tool, type
>>
>> opentheory install base
>>
>> and to upgrade an existing installation type
>>
>> opentheory update
>> opentheory upgrade
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>