diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jan 17 10:26:50 2006 +0100
+++ b/src/HOL/HOL.thy	Tue Jan 17 16:36:57 2006 +0100
@@ -1361,4 +1361,42 @@
 lemma tag_False: "tag False = False"
 by (simp add: tag_def)
 
+
+subsection {* Code generator setup *}
+
+code_alias
+  bool "HOL.bool"
+  True "HOL.True"
+  False "HOL.False"
+  "op =" "HOL.op_eq"
+  "op -->" "HOL.op_implies"
+  "op &" "HOL.op_and"
+  "op |" "HOL.op_or"
+  "op +" "IntDef.op_add"
+  "op -" "IntDef.op_minus"
+  "op *" "IntDef.op_times"
+  Not "HOL.not"
+  uminus "HOL.uminus"
+
+code_syntax_tyco bool
+  ml (atom "bool")
+  haskell (atom "Bool")
+
+code_syntax_const
+  Not
+    ml (atom "not")
+    haskell (atom "not")
+  "op &"
+    ml (infixl 1 "andalso")
+    haskell (infixl 3 "&&")
+  "op |"
+    ml (infixl 0 "orelse")
+    haskell (infixl 2 "||")
+  If
+    ml ("if __/ then __/ else __")
+    haskell ("if __/ then __/ else __")
+  "op =" (* an intermediate solution *)
+    ml (infixl 6 "=")
+    haskell (infixl 4 "==")
+
 end