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/Perm.thy
changeset 72305 6f0e85e16d84
parent 72302 d7d90ed4c74e
child 72536 589645894305 
--- a/src/HOL/Library/Perm.thy	Fri Sep 25 16:32:41 2020 +0200
+++ b/src/HOL/Library/Perm.thy	Fri Sep 25 17:13:12 2020 +0100
@@ -365,7 +365,7 @@
   then obtain B b where "affected f = insert b B"
     by blast
   with finite_affected [of f] have "card (affected f) \<ge> 1"
-    by (simp add: card_insert)
+    by (simp add: card.insert_remove)
   case False then have "order f a = 1"
     by (simp add: order_eq_one_iff)
   with \<open>card (affected f) \<ge> 1\<close> show ?thesis
isabelle