equal
deleted
inserted
replaced
1251 subsection \<open>Code module namespace\<close> |
1251 subsection \<open>Code module namespace\<close> |
1252 |
1252 |
1253 code_identifier |
1253 code_identifier |
1254 code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
1254 code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
1255 |
1255 |
1256 end |
1256 subsection \<open>Printing of evaluated natural numbers as numerals\<close> |
|
1257 |
|
1258 lemma [code_post]: |
|
1259 "Suc 0 = 1" |
|
1260 "Suc 1 = 2" |
|
1261 "Suc (numeral n) = numeral (Num.inc n)" |
|
1262 by (simp_all add: numeral_inc) |
|
1263 |
|
1264 lemmas [code_post] = Num.inc.simps |
|
1265 |
|
1266 end |