1.1 --- a/src/HOL/Library/EfficientNat.thy	Tue Jan 17 10:26:50 2006 +0100
     1.2 +++ b/src/HOL/Library/EfficientNat.thy	Tue Jan 17 16:36:57 2006 +0100
     1.3 @@ -51,6 +51,26 @@
     1.4  *}
     1.5    int ("(_)")
     1.6  
     1.7 +(* code_syntax_tyco nat
     1.8 +  ml (atom "InfInt.int")
     1.9 +  haskell (atom "Integer")
    1.10 +
    1.11 +code_syntax_const 0 :: nat
    1.12 +  ml ("0 : InfInt.int")
    1.13 +  haskell (atom "0")
    1.14 +
    1.15 +code_syntax_const Suc
    1.16 +  ml (infixl 8 "_ + 1")
    1.17 +  haskell (infixl 6 "_ + 1")
    1.18 +
    1.19 +code_primconst nat
    1.20 +ml {*
    1.21 +fun nat i = if i < 0 then 0 else i;
    1.22 +*}
    1.23 +haskell {*
    1.24 +nat i = if i < 0 then 0 else i
    1.25 +*} *)
    1.26 +
    1.27  text {*
    1.28  Case analysis on natural numbers is rephrased using a conditional
    1.29  expression: