1.1 --- a/src/HOL/HOL.thy	Tue Jan 17 10:26:50 2006 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Jan 17 16:36:57 2006 +0100
     1.3 @@ -1361,4 +1361,42 @@
     1.4  lemma tag_False: "tag False = False"
     1.5  by (simp add: tag_def)
     1.6  
     1.7 +
     1.8 +subsection {* Code generator setup *}
     1.9 +
    1.10 +code_alias
    1.11 +  bool "HOL.bool"
    1.12 +  True "HOL.True"
    1.13 +  False "HOL.False"
    1.14 +  "op =" "HOL.op_eq"
    1.15 +  "op -->" "HOL.op_implies"
    1.16 +  "op &" "HOL.op_and"
    1.17 +  "op |" "HOL.op_or"
    1.18 +  "op +" "IntDef.op_add"
    1.19 +  "op -" "IntDef.op_minus"
    1.20 +  "op *" "IntDef.op_times"
    1.21 +  Not "HOL.not"
    1.22 +  uminus "HOL.uminus"
    1.23 +
    1.24 +code_syntax_tyco bool
    1.25 +  ml (atom "bool")
    1.26 +  haskell (atom "Bool")
    1.27 +
    1.28 +code_syntax_const
    1.29 +  Not
    1.30 +    ml (atom "not")
    1.31 +    haskell (atom "not")
    1.32 +  "op &"
    1.33 +    ml (infixl 1 "andalso")
    1.34 +    haskell (infixl 3 "&&")
    1.35 +  "op |"
    1.36 +    ml (infixl 0 "orelse")
    1.37 +    haskell (infixl 2 "||")
    1.38 +  If
    1.39 +    ml ("if __/ then __/ else __")
    1.40 +    haskell ("if __/ then __/ else __")
    1.41 +  "op =" (* an intermediate solution *)
    1.42 +    ml (infixl 6 "=")
    1.43 +    haskell (infixl 4 "==")
    1.44 +
    1.45  end