src/HOL/ex/PER.thy

--- a/src/HOL/ex/PER.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/PER.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -242,7 +242,7 @@
   proof (rule someI2)
     show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
     fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
-    then have "a \<sim> x" ..
+    from this and a have "a \<sim> x" ..
     then show "x \<sim> a" ..
   qed
 qed