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

Michael Norrish michael.norrish at nicta.com.au
Mon Dec 1 23:39:59 UTC 2014

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.


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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 490 bytes
Desc: OpenPGP digital signature
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141202/8ef9416d/attachment.sig>

More information about the opentheory-users mailing list