src/HOL/Library/Executable_Set.thy
changeset 45120 717bc892e4d7
parent 45012 060f76635bfe
child 45186 645c6cac779e
     1.1 --- a/src/HOL/Library/Executable_Set.thy	Mon Oct 03 15:39:30 2011 +0200
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Mon Oct 03 22:21:19 2011 +0200
     1.3 @@ -124,6 +124,9 @@
     1.4    "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
     1.5    by (simp add: list_ex_iff)
     1.6  
     1.7 +lemma
     1.8 +  [code, code del]: "card S = card S" ..
     1.9 +
    1.10  lemma card_Set [code]:
    1.11    "card (Set xs) = length (remdups xs)"
    1.12  proof -