From 0a2a5857e365ea71a08ea467ab5216ca47cf3e00 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 10 Mar 2000 09:04:41 +0000 Subject: Updated versions. --- doc/ProofGeneral.texi | 8 ++++---- 1 file 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. -- cgit v1.2.3