# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1499758296 -7200
# Node ID a51e72d79670d88339f5d7a9dde89241dd3fa3c9
# Parent  d516da3e7c428cb3e4f3367e714a3e35607b6cdc
card_0_eq ~> fcard_0_eq

diff -r d516da3e7c42 -r a51e72d79670 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)