1.1 --- a/src/HOL/HOL.thy	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -1830,61 +1830,67 @@
     1.4  
     1.5  text {* type @{typ bool} *}
     1.6  
     1.7 -code_type bool
     1.8 -  (SML "bool")
     1.9 -  (OCaml "bool")
    1.10 -  (Haskell "Bool")
    1.11 -  (Scala "Boolean")
    1.12 -
    1.13 -code_const True and False and Not and HOL.conj and HOL.disj and HOL.implies and If 
    1.14 -  (SML "true" and "false" and "not"
    1.15 -    and infixl 1 "andalso" and infixl 0 "orelse"
    1.16 -    and "!(if (_)/ then (_)/ else true)"
    1.17 -    and "!(if (_)/ then (_)/ else (_))")
    1.18 -  (OCaml "true" and "false" and "not"
    1.19 -    and infixl 3 "&&" and infixl 2 "||"
    1.20 -    and "!(if (_)/ then (_)/ else true)"
    1.21 -    and "!(if (_)/ then (_)/ else (_))")
    1.22 -  (Haskell "True" and "False" and "not"
    1.23 -    and infixr 3 "&&" and infixr 2 "||"
    1.24 -    and "!(if (_)/ then (_)/ else True)"
    1.25 -    and "!(if (_)/ then (_)/ else (_))")
    1.26 -  (Scala "true" and "false" and "'! _"
    1.27 -    and infixl 3 "&&" and infixl 1 "||"
    1.28 -    and "!(if ((_))/ (_)/ else true)"
    1.29 -    and "!(if ((_))/ (_)/ else (_))")
    1.30 +code_printing
    1.31 +  type_constructor bool \<rightharpoonup>
    1.32 +    (SML) "bool" and (OCaml) "bool" and (Haskell) "Bool" and (Scala) "Boolean"
    1.33 +| constant True \<rightharpoonup>
    1.34 +    (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true"
    1.35 +| constant False \<rightharpoonup>
    1.36 +    (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false" 
    1.37  
    1.38  code_reserved SML
    1.39 -  bool true false not
    1.40 +  bool true false
    1.41  
    1.42  code_reserved OCaml
    1.43 -  bool not
    1.44 +  bool
    1.45  
    1.46  code_reserved Scala
    1.47    Boolean
    1.48  
    1.49 -code_modulename SML Pure HOL
    1.50 -code_modulename OCaml Pure HOL
    1.51 -code_modulename Haskell Pure HOL
    1.52 +code_printing
    1.53 +  constant Not \<rightharpoonup>
    1.54 +    (SML) "not" and (OCaml) "not" and (Haskell) "not" and (Scala) "'! _"
    1.55 +| constant HOL.conj \<rightharpoonup>
    1.56 +    (SML) infixl 1 "andalso" and (OCaml) infixl 3 "&&" and (Haskell) infixr 3 "&&" and (Scala) infixl 3 "&&"
    1.57 +| constant HOL.disj \<rightharpoonup>
    1.58 +    (SML) infixl 0 "orelse" and (OCaml) infixl 2 "||" and (Haskell) infixl 2 "||" and (Scala) infixl 1 "||"
    1.59 +| constant HOL.implies \<rightharpoonup>
    1.60 +    (SML) "!(if (_)/ then (_)/ else true)"
    1.61 +    and (OCaml) "!(if (_)/ then (_)/ else true)"
    1.62 +    and (Haskell) "!(if (_)/ then (_)/ else True)"
    1.63 +    and (Scala) "!(if ((_))/ (_)/ else true)"
    1.64 +| constant If \<rightharpoonup>
    1.65 +    (SML) "!(if (_)/ then (_)/ else (_))"
    1.66 +    and (OCaml) "!(if (_)/ then (_)/ else (_))"
    1.67 +    and (Haskell) "!(if (_)/ then (_)/ else (_))"
    1.68 +    and (Scala) "!(if ((_))/ (_)/ else (_))"
    1.69 +
    1.70 +code_reserved SML
    1.71 +  not
    1.72 +
    1.73 +code_reserved OCaml
    1.74 +  not
    1.75 +
    1.76 +code_identifier
    1.77 +  code_module Pure \<rightharpoonup>
    1.78 +    (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL
    1.79  
    1.80  text {* using built-in Haskell equality *}
    1.81  
    1.82 -code_class equal
    1.83 -  (Haskell "Eq")
    1.84 -
    1.85 -code_const "HOL.equal"
    1.86 -  (Haskell infix 4 "==")
    1.87 -
    1.88 -code_const HOL.eq
    1.89 -  (Haskell infix 4 "==")
    1.90 +code_printing
    1.91 +  type_class equal \<rightharpoonup> (Haskell) "Eq"
    1.92 +| constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "=="
    1.93 +| constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "=="
    1.94  
    1.95  text {* undefined *}
    1.96  
    1.97 -code_const undefined
    1.98 -  (SML "!(raise/ Fail/ \"undefined\")")
    1.99 -  (OCaml "failwith/ \"undefined\"")
   1.100 -  (Haskell "error/ \"undefined\"")
   1.101 -  (Scala "!sys.error(\"undefined\")")
   1.102 +code_printing
   1.103 +  constant undefined \<rightharpoonup>
   1.104 +    (SML) "!(raise/ Fail/ \"undefined\")"
   1.105 +    and (OCaml) "failwith/ \"undefined\""
   1.106 +    and (Haskell) "error/ \"undefined\""
   1.107 +    and (Scala) "!sys.error(\"undefined\")"
   1.108 +
   1.109  
   1.110  subsubsection {* Evaluation and normalization by evaluation *}
   1.111