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/Library/Infinite_Set.thy
changeset 72302 d7d90ed4c74e
parent 72097 496cfe488d72
child 75607 3c544d64c218 
--- a/src/HOL/Library/Infinite_Set.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -417,7 +417,7 @@
 proof (induction n arbitrary: S)
   case 0
   then show ?case
-    by (metis all_not_in_conv card_empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1))
+    by (metis all_not_in_conv card.empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1))
 next
   case (Suc n)
   show ?case
isabelle