removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++
authorbulwahn
Mon Oct 03 22:21:19 2011 +0200 (2011-10-03 ago)
changeset 45120717bc892e4d7
parent 45119 055c6ff9c5c3
child 45121 5e495ccf6e56
removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++
src/HOL/Library/Executable_Set.thy
     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 -