removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++
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 -