Changes for better testing

2 files changed, 26 insertions, 7 deletions

diff --git a/etc/isa/multiple/A.thy b/etc/isa/multiple/A.thy
index fc585327..b9e72899 100644
--- a/etc/isa/multiple/A.thy
+++ b/etc/isa/multiple/A.thy
@@ -4,4 +4,4 @@
     Logic Image: Pure
 *)
 
-A  =  Pure
+A  =  Main
diff --git a/etc/isa/multiple/README b/etc/isa/multiple/README
index 31b43da4..1524efce 100644
--- a/etc/isa/multiple/README
+++ b/etc/isa/multiple/README
@@ -18,9 +18,9 @@ Borrowed from Thomas's lego tests:  (v 1.2)
  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                EFFECTS A* B* C* D  D.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  
+ 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*
@@ -29,7 +29,8 @@ Borrowed from Thomas's lego tests:  (v 1.2)
 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]
-16) retract to middle of B    EFFECTS A* B+ C  D? 
+16) retract to middle of B    EFFECTS A* B+ C  D?
+	BROKEN!  Now retracts whole thing.
 14) M-x proof-restart-script  EFFECTS A  B  C  D  
 
 
@@ -48,9 +49,27 @@ to ML files of autoloaded children.
 
 
 1) visit example.ML, example.thy       ML thy
-2) assert thy			       ML thy*  (29.10.98: works, but 
-						 example.ML is on included
-						 files list: Isabelle problem)
+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)