author | paulson |
Fri, 10 Oct 2003 17:39:33 +0200 | |
changeset 14228 | a1956417c6c1 |
parent 14227 | 0356666744ec |
child 14229 | bf89038cf551 |
--- a/src/ZF/UNITY/Mutex.ML Fri Oct 10 17:39:23 2003 +0200 +++ b/src/ZF/UNITY/Mutex.ML Fri Oct 10 17:39:33 2003 +0200 @@ -99,7 +99,7 @@ (*Resulting state \\<in> n=1, p=false, m=4, u=false. Execution of V1 (the command of process v guarded by n=1) sets p:=true, violating the invariant!*) -(*Check that subgoals remain \\<in> proof failed.*) +(*Check that subgoals remain: proof failed.*) getgoal 1;