equal
deleted
inserted
replaced
66 code_syntax_const 0 :: nat |
66 code_syntax_const 0 :: nat |
67 ml (target_atom "(0:IntInf.int)") |
67 ml (target_atom "(0:IntInf.int)") |
68 haskell (target_atom "0") |
68 haskell (target_atom "0") |
69 |
69 |
70 code_syntax_const Suc |
70 code_syntax_const Suc |
71 ml (infixl 8 "_ + 1") |
71 ml (target_atom "(__ + 1)") |
72 haskell (infixl 6 "_ + 1") |
72 haskell (target_atom "(__ + 1)") |
73 |
73 |
74 text {* |
74 text {* |
75 Case analysis on natural numbers is rephrased using a conditional |
75 Case analysis on natural numbers is rephrased using a conditional |
76 expression: |
76 expression: |
77 *} |
77 *} |