diff options
| author | David Aspinall | 2000-03-10 09:04:41 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-03-10 09:04:41 +0000 |
| commit | 0a2a5857e365ea71a08ea467ab5216ca47cf3e00 (patch) | |
| tree | 8f65eda3a460c93c6e7f1658e63cf80b074fb167 | |
| parent | e7e378ec259c1e545ac1adbc8b0c46faf7747f83 (diff) | |
Updated versions.
| -rw-r--r-- | doc/ProofGeneral.texi | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index a3ea3b49..6a08ee13 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -58,10 +58,10 @@ @c @ref{node} without "see". Careful for info. -@set version 3.0 +@set version 3.1 @set xemacsversion 21.1 -@set fsfversion 20.4 -@set last-update November 1999 +@set fsfversion 20.5 +@set last-update March 2000 @set rcsid $Id$ @ifinfo @@ -2862,7 +2862,7 @@ which contain proof commands (no ML functions, structures, etc). If you do use files with Proof General which declare functions, structures, etc, you should be okay provided your code doesn't include -non-top level semi-colons (which will confuse Proof General's simplistic +non top-level semi-colons (which will confuse Proof General's simplistic parser), and provided all value declarations (and other non proof-steps) occur outside proofs. This is because within proofs, Proof General considers every ML command to be a proof step which is undoable. |