# 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"