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.
fixed proof (cf. a81f95693c68);
authorwenzelm
Thu, 18 Oct 2012 15:15:08 +0200
changeset 49922 b76937179ff5
parent 49912 c6307ee2665d
child 49923 70a2694e924f
fixed proof (cf. a81f95693c68);
src/HOL/Cardinals/Wellorder_Embedding_Base.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy	Thu Oct 18 14:15:46 2012 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy	Thu Oct 18 15:15:08 2012 +0200
@@ -722,8 +722,8 @@
                           (snd o h1) y = (snd o h2) y" by auto
     hence "(fst o h1)`(rel.underS r x) = (fst o h2)`(rel.underS r x) \<and>
            (snd o h1)`(rel.underS r x) = (snd o h2)`(rel.underS r x)"
-    by (auto simp add: image_def)
-    thus "H h1 x = H h2 x" by (simp add: H_def)
+      by (auto simp add: image_def)
+    thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball)
   qed
   (* More constant definitions:  *)
   obtain h::"'a \<Rightarrow> 'a' * bool" and f::"'a \<Rightarrow> 'a'" and g::"'a \<Rightarrow> bool"
isabelle