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/Order_Relation_More_Base.thy
changeset 51764 67f05cb13e08
parent 49310 6e30078de4f0
child 52182 57b4fdc59d3b 
--- a/src/HOL/Cardinals/Order_Relation_More_Base.thy	Wed Apr 24 16:21:23 2013 +0200
+++ b/src/HOL/Cardinals/Order_Relation_More_Base.thy	Wed Apr 24 16:43:19 2013 +0200
@@ -63,7 +63,7 @@
   (*  *)
   fix a assume *: "a \<in> Field r"
   obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a"
-  using * 1 by blast
+  using * 1 by auto
   hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT
   by (simp add: total_on_def)
   thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast
isabelle