Merge changes from Version4Branch.

12 files changed, 0 insertions, 167 deletions

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;