Deleted file

1 files changed, 0 insertions, 68 deletions

diff --git a/isa/BUGS b/isa/BUGS
deleted file mode 100644
index 41f992c3..00000000
--- a/isa/BUGS
+++ /dev/null
@@ -1,68 +0,0 @@
--*- mode:outline -*-
-
-* Isabelle Proof General Bugs
-
-See also ../BUGS for generic bugs.
-
-See also ../isar/BUGS.  Isar is now main the instance for 
-Isabelle PG, the original Isabelle instance less supported.
-
-
-** Issues with tracing mode 
-
-1. Large volumes of output can cause Emacs to hog CPU spending
-all its time processing the output (esp with fontifying and X-symbol
-decoding).   It becomes difficult to use normal editing commands,
-even C-c C-c to interrupt the prover.  Workaround: hitting C-g,
-the Emacs quit key, will interrupt the prover in this state.
-See manual for further description of this.
-
-2. Interrupt response may be lost in large volumes of output, when
-using pty communication.  Symptom is interrupt on C-g, but PG thinks
-the prover is still busy.  Workaround: hit return in the shell buffer,
-or set proof-shell-process-connection-type to nil to use piped
-communication.
-
-** set proof_timing is problematic
-
-It will make the goals display disappear during proof.  This is
-because Proof General only displays goals output that appears *after*
-Isabelle messages, but Isabelle prints the timing message after the
-goals are displayed.
-
-** General difficulty with proof scripts containing ML structures, 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.  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
-theory file (and it's ancestors) to be read as scripting is turned on.
-To avoid this, assert the theory file rather than the ML file.
-
-** Subsection Interaction with theory database
-
-Isabelle Proof General uses some support from Isabelle to remove and
-reload theories from the theory database.  To maintain consistency,
-Isabelle is rather conservative.  So re-asserting a retracted file will
-often re-load it, even if it has not changed.  (This is because the
-file may have implicit dependencies on things in the global ML
-environment not made apparent by the theory structure).  
-This may lead to seemingly unnecessary repetition of time-consuming
-proofs, so be careful not to retract more than you need!
-
-As of Isabelle 99-1 and Proof General 3.2, there should be much
-less unncessary re-loading of theories; be careful to use Isabelle's
-mechanisms of declaring dependencies in theory file headers.
-
-** Clash with SML mode
-
-Since Isabelle proof scripts are not differentiated from `.ML' files,
-Proof General may compete with `sml-mode' (if you use it) for
-controlling these buffers.  To ensure Proof General wins, load it last.
-
-Workaround: use another extension for real ML files, e.g.  `.sml',
-and disable `.ML' from entering `sml-mode'.