From e0706d87ee5550e452c964fffb240aa74a2aa9b7 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 6 Oct 1999 10:52:43 +0000
Subject: Note to use C-c C-s to solve Isabelle prob

---
 BUGS | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'BUGS')

diff --git a/BUGS b/BUGS
index 33fef98e..2e002cd9 100644
--- a/BUGS
+++ b/BUGS
@@ -163,7 +163,8 @@ interface unless you use your own "goal" or "qed" forms.
 * Blocking when processing multiple files, beginning from a .ML file.
 Proof General will block the Emacs process when it is waiting for
 a theory file (and it's ancestors) to be read.  To avoid this,
-assert the theory file rather than the ML file.
+assert the theory file rather than the ML file, or use C-c C-s
+to start scripting before using one of the assertion commands.
 
 * Cut-and-paste from Isabelle output (e.g. goals buffer) is
 problematic.  You will find that this inserts otherwise-invisible
-- 
cgit v1.2.3