From 3d28f91919372c2ca54e097be8836f8530388594 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 29 Nov 1999 14:05:02 +0000
Subject: Added more notes about using ML files in Isabelle.

---
 BUGS | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'BUGS')

diff --git a/BUGS b/BUGS
index 3771b5df..0fb4e142 100644
--- a/BUGS
+++ b/BUGS
@@ -150,14 +150,11 @@ goals output that appears *after* Isabelle messages, but Isabelle
 prints the timing message after the goals are displayed.
 
 * There is a general difficulty with proof scripts containing ML
-structures, functions, etc.  Proof General does not understand full ML
-syntax(!), so it will be confused by structures which contain 
+structures, functions, etc.  Proof General does not understand full
+ML syntax(!), so it will be confused by structures which contain
 semi-colons after declarations, for example.  Also, it cannot undo
-function declarations.  Moreover, with ML you can even redefine
-the entire proof command language, which will certainly confuse
-Proof General!  Stick to using the standard functions, tactics, and
-tacticals and there should be no problems.  (Actually, there should
-be no problems unless you use your own "goal" or "qed" forms).
+function declarations.  See the section on ML files in the manual
+for more details.
 
 * Blocking when processing multiple files, beginning from a .ML file.
 Proof General will block the Emacs process when it is waiting for a
-- 
cgit v1.2.3