Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Cardinals/Wellorder_Embedding_Base.thy
changeset 51764 67f05cb13e08
parent 49922 b76937179ff5 
--- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -683,7 +683,7 @@
     have "wo_rel.ofilter r (rel.underS r ?a)"
     using Well by (auto simp add: wo_rel.underS_ofilter)
     ultimately
-    have "False \<notin> g`(rel.under r b)" using 3 Well by (auto simp add: wo_rel.ofilter_def)
+    have "False \<notin> g`(rel.under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+
     moreover have "b \<in> Field r"
     unfolding Field_def using as by (auto simp add: rel.underS_def)
     ultimately
isabelle