card_0_eq ~> fcard_0_eq
authorLars Hupel <lars.hupel@mytum.de>
Tue, 11 Jul 2017 09:31:36 +0200
changeset 66265 a51e72d79670
parent 66264 d516da3e7c42
child 66266 130dea8500cb
card_0_eq ~> fcard_0_eq
src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Tue Jul 11 09:22:14 2017 +0200
+++ b/src/HOL/Library/FSet.thy	Tue Jul 11 09:31:36 2017 +0200
@@ -606,7 +606,7 @@
   "fcard (finsert x A) = (if x |\<in>| A then fcard A else Suc (fcard A))"
   by transfer (rule card_insert_if)
 
-lemma card_0_eq [simp, no_atp]:
+lemma fcard_0_eq [simp, no_atp]:
   "fcard A = 0 \<longleftrightarrow> A = {||}"
   by transfer (rule card_0_eq)