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

[Michael Norrish]

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
> 


-------------- 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>