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/Set_Interval.thy
changeset 72302 d7d90ed4c74e
parent 72268 71a8935eb5da
child 72686 703b601d71b5 
--- a/src/HOL/Set_Interval.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -1538,7 +1538,7 @@
   also have "\<dots> = Suc (card ({k \<in> M. k < Suc i} - {0}))"
     by (force intro: arg_cong [where f=card])
   also have "\<dots> = card (insert 0 ({k \<in> M. k < Suc i} - {0}))"
-    by (simp add: card_insert)
+    by (simp add: card.insert_remove)
   also have "... = card {k \<in> M. k < Suc i}"
     using assms
     by (force simp add: intro: arg_cong [where f=card])
isabelle