equal
deleted
inserted
replaced
250 ML "timeit (@{code test} 25)" |
250 ML "timeit (@{code test} 25)" |
251 ML "timeit (@{code test'} 25)" |
251 ML "timeit (@{code test'} 25)" |
252 ML "timeit (@{code test} 500)" |
252 ML "timeit (@{code test} 500)" |
253 ML "timeit @{code test''}" |
253 ML "timeit @{code test''}" |
254 |
254 |
|
255 text {* the same story with the legacy SML code generator. |
|
256 this can be removed once the code generator is removed. |
|
257 *} |
|
258 |
255 consts_code |
259 consts_code |
256 "default :: nat" ("{* 0::nat *}") |
260 "default :: nat" ("{* 0::nat *}") |
257 "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}") |
261 "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}") |
258 |
262 |
259 code_module PH |
263 code_module PH |