Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++
authorbulwahn
Mon, 03 Oct 2011 22:21:19 +0200
changeset 45120 717bc892e4d7
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 file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Executable_Set.thy	Mon Oct 03 15:39:30 2011 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Mon Oct 03 22:21:19 2011 +0200
@@ -124,6 +124,9 @@
   "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
   by (simp add: list_ex_iff)
 
+lemma
+  [code, code del]: "card S = card S" ..
+
 lemma card_Set [code]:
   "card (Set xs) = length (remdups xs)"
 proof -
isabelle