diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-12-11 17:14:10 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-12-11 17:14:10 +0000 |
| commit | 1a10f19e8a61388e74ecc60bf603753cb06681fe (patch) | |
| tree | d0e7cc38bdcbd64782e6436f7f71f527409a7d64 /etc/isa/multiple | |
| parent | 48f9b4c9c0196f8720a9ac518e4eb4c80d3000e0 (diff) | |
More test cases mentioned
Diffstat (limited to 'etc/isa/multiple')
| -rw-r--r-- | etc/isa/multiple/README | 26 |
1 files changed, 26 insertions, 0 deletions
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. + + + |