PGIPCommentary < PG

PG Web>PGIP>PGIPBasicProverModel>PGIPCommentary (22 Aug 2006, DavidAspinall) (raw view)EditAttach

---+ !PGIP Commentary

The commentary on the PGIP syntax specification explains the meaning of PGIP commands.

It is available as a [[http://proofgeneral.inf.ed.ac.uk/kit/docs/commentary.pdf][pdf file]]
on the main PG kit page, http://proofgeneral.inf.ed.ac.uk/kit

---++ Supplemental information (pending improvements)

Things to be added/clarified in the commentary include:

   * Include the PGIPBasicProverModel diagram and some explanation 
   * Include configuration for specifying undo behaviour for efficiency
   * Include configuration for specifying nested proof behaviour (maybe as in ProofGeneralEmacs).
 
See PGIPDevelNotes for more details and discussions on more tentative extensions.
 
---++ Questions, comments suggestions

Please add questions/comments/requests for improvements about the commentary in
subsections here.

Topic revision: r2 - 22 Aug 2006 - 13:41:13 - DavidAspinall

Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies