From 1a10f19e8a61388e74ecc60bf603753cb06681fe Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 11 Dec 1998 17:14:10 +0000 Subject: More test cases mentioned --- etc/isa/multiple/README | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) (limited to 'etc/isa/multiple') diff --git a/etc/isa/multiple/README b/etc/isa/multiple/README index a50c063d..8ffa6fba 100644 --- a/etc/isa/multiple/README +++ b/etc/isa/multiple/README @@ -29,6 +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] + 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 @@ -74,3 +76,27 @@ to ML files of autoloaded children. + +----------------------------------------------------------------- + +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. + + + -- cgit v1.2.3