Merge changes from Version4Branch.

1 files changed, 0 insertions, 102 deletions

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.
-
-
-