obsolete;

1 files changed, 0 insertions, 43 deletions

diff --git a/etc/isa/completed-proof.ML b/etc/isa/completed-proof.ML
deleted file mode 100644
index 70cc8e18..00000000
--- a/etc/isa/completed-proof.ML
+++ /dev/null
@@ -1,43 +0,0 @@
-(* Test of completed proof behaviour: even if qed command is missing,
-   PG should close of the proof as a goalsave.
-
-   Issue with Isabelle2002: Goals.disable_pr prevents
-   proof-shell-proof-completed being set because "No Subgoals!" is not
-   displayed.  This means that processing file in one go here (or C-c
-   C-RET at val_) does not work properly.
-*)
-
-(* default proof-completed-proof-behaviour for isa is 'closeany. 
-   Also should test this file with 'closegoal, 'extend.
-      
-    (setq proof-completed-proof-behaviour 'closeany)  
-     : close on any command after proof completed seen
-    (setq proof-completed-proof-behaviour 'closegoal)
-     : close when next goal is seen
-    (setq proof-completed-proof-behaviour 'extend)
-     : continually extend region after proof completed, until next goal.
-
- *)
-
-Goal "A & B --> B & A";
-  by (rtac impI 1);
-  by (etac conjE 1);
-  by (rtac conjI 1);
-  by (assume_tac 1);
-  by (assume_tac 1);
-  (* qed "and_comms"; *)
-
-val _ = ();
-val _ = ();
-
-Goal "A & B --> B & A";
-  by (rtac impI 1);
-  by (etac conjE 1);
-  by (rtac conjI 1);
-  by (assume_tac 1);
-  by (assume_tac 1);
-  qed "and_comms";
-
-
-
-