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/Fun_More_FP.thy
changeset 54482 a2874c8b3558
parent 54481 5c9819d7713b
child 54578 9387251b6a46 
--- a/src/HOL/Cardinals/Fun_More_FP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Fun_More_FP.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -232,7 +232,7 @@
 using assms
 using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
       card_atLeastLessThan[of m] card_atLeastLessThan[of n]
-      card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by auto
+      card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce
isabelle