src/HOL/Datatype.thy
changeset 19150 1457d810b408
parent 19138 42ff710d432f
child 19179 61ef97e3f531
     1.1 --- a/src/HOL/Datatype.thy	Mon Feb 27 15:49:56 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Mon Feb 27 15:51:37 2006 +0100
     1.3 @@ -286,6 +286,33 @@
     1.4      ml (target_atom "(__,/ __)")
     1.5      haskell (target_atom "(__,/ __)")
     1.6  
     1.7 +code_generate Unity
     1.8 +
     1.9 +code_syntax_tyco
    1.10 +  unit
    1.11 +    ml (target_atom "unit")
    1.12 +    haskell (target_atom "()")
    1.13 +
    1.14 +code_syntax_const
    1.15 +  Unity
    1.16 +    ml (target_atom "()")
    1.17 +    haskell (target_atom "()")
    1.18 +
    1.19 +code_generate None Some
    1.20 +
    1.21 +code_syntax_tyco
    1.22 +  option
    1.23 +    ml ("_ option")
    1.24 +    haskell ("Maybe _")
    1.25 +
    1.26 +code_syntax_const
    1.27 +  None
    1.28 +    ml (target_atom "NONE")
    1.29 +    haskell (target_atom "Nothing")
    1.30 +  Some
    1.31 +    ml (target_atom "SOME")
    1.32 +    haskell (target_atom "Just")
    1.33 +
    1.34  code_syntax_const
    1.35    "1 :: nat"
    1.36      ml ("{*Suc 0*}")