--- a/src/HOL/Datatype.thy Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/Datatype.thy Wed Jun 14 12:14:42 2006 +0200
@@ -257,14 +257,11 @@
fst_conv [code]
snd_conv [code]
-lemma [code unfolt]:
- "1 == Suc 0" by simp
-
-code_syntax_tyco bool
+code_typapp bool
ml (target_atom "bool")
haskell (target_atom "Bool")
-code_syntax_const
+code_constapp
True
ml (target_atom "true")
haskell (target_atom "True")
@@ -284,32 +281,32 @@
ml (target_atom "(if __/ then __/ else __)")
haskell (target_atom "(if __/ then __/ else __)")
-code_syntax_tyco
+code_typapp
*
ml (infix 2 "*")
haskell (target_atom "(__,/ __)")
-code_syntax_const
+code_constapp
Pair
ml (target_atom "(__,/ __)")
haskell (target_atom "(__,/ __)")
-code_syntax_tyco
+code_typapp
unit
ml (target_atom "unit")
haskell (target_atom "()")
-code_syntax_const
+code_constapp
Unity
ml (target_atom "()")
haskell (target_atom "()")
-code_syntax_tyco
+code_typapp
option
ml ("_ option")
haskell ("Maybe _")
-code_syntax_const
+code_constapp
None
ml (target_atom "NONE")
haskell (target_atom "Nothing")
--- a/src/HOL/HOL.thy Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/HOL.thy Wed Jun 14 12:14:42 2006 +0200
@@ -1412,7 +1412,7 @@
Not "HOL.not"
arbitrary "HOL.arbitrary"
-code_syntax_const
+code_constapp
"op =" (* an intermediate solution for polymorphic equality *)
ml (infixl 6 "=")
haskell (infixl 4 "==")
--- a/src/HOL/Lambda/WeakNorm.thy Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Wed Jun 14 12:14:42 2006 +0200
@@ -501,7 +501,7 @@
arbitrary :: "'a" ("(error \"arbitrary\")")
arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
-code_syntax_const
+code_constapp
"arbitrary :: 'a" ml (target_atom "(error \"arbitrary\")")
"arbitrary :: 'a \<Rightarrow> 'b" ml (target_atom "(fn '_ => error \"arbitrary\")")
--- a/src/HOL/List.thy Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/List.thy Wed Jun 14 12:14:42 2006 +0200
@@ -2737,17 +2737,17 @@
"List.op @" "List.append"
"List.op mem" "List.mem"
-code_syntax_tyco
+code_typapp
list
ml ("_ list")
haskell (target_atom "[_]")
-code_syntax_const
+code_constapp
Nil
ml (target_atom "[]")
haskell (target_atom "[]")
-code_syntax_tyco
+code_typapp
char
ml (target_atom "char")
haskell (target_atom "Char")
--- a/src/HOL/Nat.thy Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/Nat.thy Wed Jun 14 12:14:42 2006 +0200
@@ -601,7 +601,8 @@
lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
by (induct m) simp_all
-lemma [code]: "Suc m + n = m + Suc n" by simp
+lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
+ by simp
text {* Associative law for addition *}
--- a/src/HOL/Wellfounded_Recursion.thy Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy Wed Jun 14 12:14:42 2006 +0200
@@ -295,7 +295,7 @@
CodegenPackage.add_appconst ("wfrec", ((3, 3), CodegenPackage.appgen_wfrec))
*}
-code_syntax_const
+code_constapp
wfrec
ml ("let fun wfrec f x = f (wfrec f) x in wfrec _ _ end;")
haskell ("wfrec _ _ where wfrec f x = f (wfrec f) x")