changeset 19137 | f92919b141b2 |
parent 19041 | 1a8f08f9f8af |
child 19481 | a6205c6203ea |
--- a/src/HOL/Library/EfficientNat.thy Sat Feb 25 15:19:00 2006 +0100 +++ b/src/HOL/Library/EfficientNat.thy Sat Feb 25 15:19:19 2006 +0100 @@ -63,7 +63,7 @@ ml (target_atom "IntInf.int") haskell (target_atom "Integer") -code_syntax_const 0 :: nat +code_syntax_const "0 :: nat" ml (target_atom "(0:IntInf.int)") haskell (target_atom "0")