Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Wed, 07 Feb 2001 20:57:03 +0100
changeset 11083 d8fda557e476
parent 11082 9a7cdfaa7ecb
child 11084 32c1deea5bcd
tuned;
src/HOL/subset.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle