--- a/src/HOL/Datatype.thy Wed Jun 07 16:54:30 2006 +0200
+++ b/src/HOL/Datatype.thy Wed Jun 07 16:55:14 2006 +0200
@@ -219,20 +219,20 @@
done
+subsubsection {* Codegenerator setup *}
+
consts
is_none :: "'a option \<Rightarrow> bool"
primrec
"is_none None = True"
"is_none (Some x) = False"
-(* lemma is_none_none [code unfolt]:
+lemma is_none_none [code unfolt]:
"(x = None) = (is_none x)"
-by (cases "x") simp_all *)
+by (cases "x") simp_all
lemmas [code] = imp_conv_disj
-subsubsection {* Codegenerator setup *}
-
lemma [code fun]:
"(\<not> True) = False" by (rule HOL.simp_thms)
@@ -260,8 +260,6 @@
lemma [code unfolt]:
"1 == Suc 0" by simp
-code_generate True False Not "op &" "op |" If
-
code_syntax_tyco bool
ml (target_atom "bool")
haskell (target_atom "Bool")
@@ -286,8 +284,6 @@
ml (target_atom "(if __/ then __/ else __)")
haskell (target_atom "(if __/ then __/ else __)")
-code_generate Pair
-
code_syntax_tyco
*
ml (infix 2 "*")
@@ -298,8 +294,6 @@
ml (target_atom "(__,/ __)")
haskell (target_atom "(__,/ __)")
-code_generate Unity
-
code_syntax_tyco
unit
ml (target_atom "unit")
@@ -310,8 +304,6 @@
ml (target_atom "()")
haskell (target_atom "()")
-code_generate None Some
-
code_syntax_tyco
option
ml ("_ option")
@@ -325,7 +317,4 @@
ml (target_atom "SOME")
haskell (target_atom "Just")
-
-
-
end