# HG changeset patch
# User paulson
# Date 1065800373 -7200
# Node ID a1956417c6c175ceda196b2ca1e7b7d66da84896
# Parent  0356666744ecea4cbbb79644c43b6873785abf9c
trivial

diff -r 0356666744ec -r a1956417c6c1 src/ZF/UNITY/Mutex.ML
--- 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;