src/HOL/Datatype.thy

--- a/src/HOL/Datatype.thy	Tue Jan 17 10:26:50 2006 +0100
+++ b/src/HOL/Datatype.thy	Tue Jan 17 16:36:57 2006 +0100
@@ -220,4 +220,24 @@
 
 lemmas [code] = imp_conv_disj
 
+subsubsection {* Codegenerator setup *}
+
+code_syntax_const
+  True
+    ml (atom "true")
+    haskell (atom "True")
+  False
+    ml (atom "false")
+    haskell (atom "False")
+
+code_syntax_const
+  Pair
+    ml (atom "(__,/ __)")
+    haskell (atom "(__,/ __)")
+
+code_syntax_const
+  1 :: "nat"
+    ml ("{*Suc 0*}")
+    haskell ("{*Suc 0*}")
+
 end