20 files changed, 0 insertions, 272 deletions
diff --git a/etc/isa/\backslashname/test.ML b/etc/isa/\backslashname/test.ML
deleted file mode 100644
index 0691e38e..00000000
--- a/etc/isa/\backslashname/test.ML
+++ /dev/null
@@ -1,11 +0,0 @@
-(* Scripting here tests quotation mechanism for filenames. *)
-
-(* At the moment this trips a bug in Isabelle which objects
-   to filename of this directory.
-
-   Easy way to test for other provers is with a link,
-   \bizzare  \\<rightarrow> ProofGeneral/  then load \bizarre/coq/example.v, etc
-
-*)
-
-val a = 1;
diff --git a/etc/isa/\backslashname/test.thy b/etc/isa/\backslashname/test.thy
deleted file mode 100644
index 2ca5331f..00000000
--- a/etc/isa/\backslashname/test.thy
+++ /dev/null
@@ -1 +0,0 @@
-test = Pure
diff --git a/etc/isa/long-line-backslash.ML b/etc/isa/long-line-backslash.ML
deleted file mode 100644
index 66435c1b..00000000
--- a/etc/isa/long-line-backslash.ML
+++ /dev/null
@@ -1,20 +0,0 @@
-(* 
-
-  long-line-backslash.ML
-
-  Test for long lines with backslashes in them.
-  Cause problem with pty communication where line length
-  is limited to 256 characters sometimes (e.g. on Solaris).
-
-*)
-
-val nasty_string="\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\";
-
-(* Test subsequent commands can be processed *)
-
-val one = 1;
-val two = 2;
-val three = 3;
-
-(* Test something with eager annotations *)
-
diff --git a/etc/isa/message-test.ML b/etc/isa/message-test.ML
deleted file mode 100644
index 4afd7120..00000000
--- a/etc/isa/message-test.ML
+++ /dev/null
@@ -1,16 +0,0 @@
-(* Testing different kinds of markup in Isabelle output *)
-
-(* ordinary output between prompts *)
-print "ordinary";
-print "ordinary\n";   (* final newline no difference *)
-
-(* eager annotation: displayed as soon as it's seen *)
-writeln "eager to be seen!";
-
-print "more ordinary\n";
-
-Goal "P-->P";
-
-(* C-c RET to here should show eager annotation, as well as
-   updating goals buffer properly. *)
-error "something went wrong";  
diff --git a/etc/isa/multiple/A.ML b/etc/isa/multiple/A.ML
deleted file mode 100644
index 771a5f1a..00000000
--- a/etc/isa/multiple/A.ML
+++ /dev/null
@@ -1,11 +0,0 @@
-(* Scripting buffer for theory A *)
-
-1;
-
-(* A few commands so that we can test partial-retraction. *)
-
-2;
-
-3;
-
-
diff --git a/etc/isa/multiple/A.thy b/etc/isa/multiple/A.thy
deleted file mode 100644
index fc585327..00000000
--- a/etc/isa/multiple/A.thy
+++ /dev/null
@@ -1,7 +0,0 @@
-(* 
-    File:	 /home/da/proofgen/ProofGeneral/etc/isa/multiple/A.thy
-    Theory Name: A
-    Logic Image: Pure
-*)
-
-A  =  Pure
diff --git a/etc/isa/multiple/B.ML b/etc/isa/multiple/B.ML
deleted file mode 100644
index e0226516..00000000
--- a/etc/isa/multiple/B.ML
+++ /dev/null
@@ -1,4 +0,0 @@
-(* Scripting buffer for theory B *)
-
-val b = 0;
-val b1 = 1;
diff --git a/etc/isa/multiple/B.thy b/etc/isa/multiple/B.thy
deleted file mode 100644
index a896bca2..00000000
--- a/etc/isa/multiple/B.thy
+++ /dev/null
@@ -1,7 +0,0 @@
-(* 
-    File:	 /home/da/proofgen/ProofGeneral/etc/isa/multiple/B.thy
-    Theory Name: B
-    Logic Image: Pure
-*)
-
-B  =  Pure
diff --git a/etc/isa/multiple/C.ML b/etc/isa/multiple/C.ML
deleted file mode 100644
index 4ad965a2..00000000
--- a/etc/isa/multiple/C.ML
+++ /dev/null
@@ -1,4 +0,0 @@
-(* Scripting buffer for theory C *)
-
-val c1 = 4;
-val c = 5;
diff --git a/etc/isa/multiple/C.thy b/etc/isa/multiple/C.thy
deleted file mode 100644
index 3316eaee..00000000
--- a/etc/isa/multiple/C.thy
+++ /dev/null
@@ -1,10 +0,0 @@
-(* 
-    File:	 /home/da/proofgen/ProofGeneral/etc/isa/multiple/C.thy
-    Theory Name: C
-    Logic Image: Pure
-*)
-
-theory C  =  A + B
-files "foobar/foo.ML":
-
-end
diff --git a/etc/isa/multiple/D.ML b/etc/isa/multiple/D.ML
deleted file mode 100644
index 76dd89c1..00000000
--- a/etc/isa/multiple/D.ML
+++ /dev/null
@@ -1,3 +0,0 @@
-(* Scripting buffer for theory D *)
-
-val it = ();
diff --git a/etc/isa/multiple/D.thy b/etc/isa/multiple/D.thy
deleted file mode 100644
index afacc20e..00000000
--- a/etc/isa/multiple/D.thy
+++ /dev/null
@@ -1,7 +0,0 @@
-(* 
-    File:	 /home/da/proofgen/ProofGeneral/etc/isa/multiple/D.thy
-    Theory Name: D
-    Logic Image: Pure
-*)
-
-D  =  Pure
diff --git a/etc/isa/multiple/Err.ML b/etc/isa/multiple/Err.ML
deleted file mode 100644
index 177da5ce..00000000
--- a/etc/isa/multiple/Err.ML
+++ /dev/null
@@ -1,5 +0,0 @@
-(* Test to see that scripting is *not* turned on
-   if an error occurs during activation
-*)
-
-val x = 1;
diff --git a/etc/isa/multiple/Err.thy b/etc/isa/multiple/Err.thy
deleted file mode 100644
index d36a5af2..00000000
--- a/etc/isa/multiple/Err.thy
+++ /dev/null
@@ -1,3 +0,0 @@
-(* Dummy file to cause an error in use_thy *)
-
-Err = blah
-\ No newline at end of file
diff --git a/etc/isa/multiple/README b/etc/isa/multiple/README
deleted file mode 100644
index 8ffa6fba..00000000
--- a/etc/isa/multiple/README
+++ /dev/null
@@ -1,102 +0,0 @@
-Test files for multiple file handling with Isabelle.
-
-
-Test schedule
-=============
-
-[C depends on A and B, D is independent]
-
-Notation: A  means that buffer A.l is unlocked
-          A+ means that buffer A.l is partly locked
-          A* means that buffer A.l is locked
-	  ? means that behaviour might be different for proof systems
-  	    with non-linear contexts
-
-Borrowed from Thomas's lego tests:  (v 1.2)
-
- 1) visit A.ML                EFFECTS A
- 2) visit C.ML                EFFECTS A     C
- 3) assert C                  EFFECTS A*    C*
- 4) visit B.ML,B.thy,C.thy    EFFECTS A* B* C*    C.thy* B.thy*
- 5) visit D.ML,D.thy          EFFECTS A* B* C* D  D.thy
- 6) retract to middle of B    EFFECTS A* B  C  D  B.thy* (*thy remains locked*)
- 7) assert first command of B EFFECTS A* B+ C  D
- 8) assert C                  EFFECTS A* B+ C  D [error message, correctly]
- 9) assert B                  EFFECTS A* B* C  D 
-10) assert D                  EFFECTS A* B* C  D*  D.thy*
-11) retract B                 EFFECTS A* B  C  D? [D* D.thy* for Isabelle]
-12) assert C                  EFFECTS A* B* C* D? 
-13) retract B                 EFFECTS A* B  C  D? [B.thy* D*,D.thy* again]
-14) assert B                  EFFECTS A* B* C  D? 
-15) assert C                  EFFECTS A* B* C* D? [everything locked]
-        BROKEN 11.12.98: B.ML *may* not be locked?
- 
-16) retract to middle of B    EFFECTS A* B+ C  D?
-	BROKEN!  Now retracts whole thing.
-14) M-x proof-shell-restart   EFFECTS A  B  C  D  
-
-
-MORE TESTS NEEDED FOR ISABELLE:
-===============================
-
-Should test assertion of theory files, and watch what happens to ML files.
-
-Because of theory loader's odd behaviour, must watch what happens
-to ML files of autoloaded children.
-
-
-1) visit example.ML, example.thy       EFFECT: ML thy
-2) assert .ML			       EFFECT: ML* thy*
-3) retract thy			       EFFECT: ML thy
-
-
-1) visit example.ML, example.thy       ML thy
-2) assert thy			       ML* thy*   (reads theory too)
-
-
-(* Test case for outdating a child theory *)
-
-1) assert C.thy		        A*, B*, C*
-2) retract B.thy		A*
-3) edit B.thy to touch timestamp
-4) assert B.thy			A*, B*, C  Message: "C out of date"
-5) assert C.thy			A*, B*, C*
-
-
-(* Test case for removing a dependency from a theory:
-   this automatically unlocks the orphaned theory,
-   is this right??
-*)   
-
-1) assert C.thy			A*, B*, C*
-2) retract C.thy		A*, B*, C
-3) edit C.thy to C=A, remove dependency on B
-4) assert C.thy		        A*, B, C*      (B automatically unlocked)
-
-
-
-
-
------------------------------------------------------------------
-
-Question:
-
-We assert script A.
-We assert script B.
-Can we retract to middle of A?  Yes, we should be able to!
-
-
-
------------------------------------------------------------------
-
-Tester:
-
-Visit A.ML.  Assert partly.
-
-Visit C.thy.  Assert it.
-
-This should lock remainder of A.ML, since it has now been read
-completely.
-
-
-
diff --git a/etc/isa/multiple/foobar/foo.ML b/etc/isa/multiple/foobar/foo.ML
deleted file mode 100644
index 25084a22..00000000
--- a/etc/isa/multiple/foobar/foo.ML
+++ /dev/null
@@ -1,4 +0,0 @@
-
-val foo = "foo";
-
-val bar = 1;
diff --git a/etc/isa/parsing.ML b/etc/isa/parsing.ML
deleted file mode 100644
index 805e69fb..00000000
--- a/etc/isa/parsing.ML
+++ /dev/null
@@ -1,13 +0,0 @@
-(* Any (* nested comments *) are tricky in XEmacs (21.4.8),
-   but better syntax handling in Emacs at the moment.
-*)
-
-Goal "A \\<and> B \\<longrightarrow> B \\<and> A";
-by (rtac impI 1);
-by (etac conjE 1);
-by (rtac conjI 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "and_comms";
-
-(* Comment at the end?! *)
-\ No newline at end of file
diff --git a/etc/isa/settings.ML b/etc/isa/settings.ML
deleted file mode 100644
index 3250f9ca..00000000
--- a/etc/isa/settings.ML
+++ /dev/null
@@ -1,21 +0,0 @@
-(* 
-   Simple test for variable setting mechanism ML -> PG. 
-   This kind of protocol is included in PGIP for setting config variables.
-   Here we can use it for executing arbitrary elisp, in fact (eek!)
-*)
-
-fun pg_setvar var exp = writeln ("Proof General, please set the variable " ^ var ^ " to: #" ^ exp ^ "#.");
-
-pg_setvar "wag" "(+ 33 44)";   (* C-h v wag RET gives 77 *)
-
-fun pgset var = pg_setvar var "t";
-fun pgreset var = pg_setvar var "nil";
-
-pgset "isa-show-types";    (* sets show-types in menu *)
-
-(* What might be nice is to override 'set' 'reset' fuctions to mirror
-   settings in PG automatically, but then we'd need to retrieve the
-   names of the ML values from the 'set' and 'reset' functions... *)
-
-(* test failure case: prints a debug message if proof-show-debug-messages<>nil *)
-pg_setvar "wig" "blah 12 x12"
diff --git a/etc/isa/thy/test.ML b/etc/isa/thy/test.ML
deleted file mode 100644
index 6a434570..00000000
--- a/etc/isa/thy/test.ML
+++ /dev/null
@@ -1,5 +0,0 @@
-(* Test case for wrong file type
-   bug report by jv@ddre.dk
-
-   This file should be ML, not theory!
-*)
-\ No newline at end of file
diff --git a/etc/isa/xsym.ML b/etc/isa/xsym.ML
deleted file mode 100644
index 797bad69..00000000
--- a/etc/isa/xsym.ML
+++ /dev/null
@@ -1,18 +0,0 @@
-(* a few token characters to exercise X-Symbol *)
-
-Goal "A \\<and> B  \\<longrightarrow> B \\<and> A";
-by (rtac impI 1);
-by (etac conjE 1);
-by (rtac conjI 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "and_comms";
-
-3;
-
-4;
-
-print "hello";
-
-writeln "hello";
-error "hello";