# HG changeset patch
# User wenzelm
# Date 981575823 -3600
# Node ID d8fda557e4761ae28ec892fe26ead6aa99b11f36
# Parent  9a7cdfaa7ecbe0850f8483b1ca54f190beb7b32e
tuned;

diff -r 9a7cdfaa7ecb -r d8fda557e476 src/HOL/subset.thy
--- a/src/HOL/subset.thy	Wed Feb 07 20:56:40 2001 +0100
+++ b/src/HOL/subset.thy	Wed Feb 07 20:57:03 2001 +0100
@@ -66,8 +66,8 @@
   proof
     assume "Abs x = Abs y"
     hence "Rep (Abs x) = Rep (Abs y)" by simp
-    moreover note x hence "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])
-    moreover note y hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
+    moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])
+    moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
     ultimately show "x = y" by (simp only:)
   next
     assume "x = y"