equal
deleted
inserted
replaced
572 text {* |
572 text {* |
573 The same story again for code next generation. |
573 The same story again for code next generation. |
574 *} |
574 *} |
575 |
575 |
576 setup {* |
576 setup {* |
577 CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")" |
577 CodeTarget.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")" |
578 *} |
578 *} |
579 |
579 |
580 definition |
580 definition |
581 int :: "nat \<Rightarrow> int" where |
581 int :: "nat \<Rightarrow> int" where |
582 "int \<equiv> of_nat" |
582 "int \<equiv> of_nat" |