src/HOL/Library/FSet.thy

 
 (* FIXME: improve transferred to handle bounded meta quantification *)
 
 lemma fcard_fempty:
   "fcard {||} = 0"
-  by transfer (rule card_empty)
+  by transfer (rule card.empty)
 
 lemma fcard_finsert_disjoint:
   "x |\<notin>| A \<Longrightarrow> fcard (finsert x A) = Suc (fcard A)"
   by transfer (rule card_insert_disjoint)
 

   assumes "a |\<in>| A" and "a |\<notin>| B"
   shows "fcard (A |-| finsert a B) = fcard (A |-| B) - 1"
 using assms by transfer (rule card_Diff_insert)
 
 lemma fcard_finsert: "fcard (finsert x A) = Suc (fcard (A |-| {|x|}))"
-by transfer (rule card_insert)
+by transfer (rule card.insert_remove)
 
 lemma fcard_finsert_le: "fcard A \<le> fcard (finsert x A)"
 by transfer (rule card_insert_le)
 
 lemma fcard_mono: