equal
deleted
inserted
replaced
764 and (Eval) "abs" |
764 and (Eval) "abs" |
765 |
765 |
766 code_identifier |
766 code_identifier |
767 code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
767 code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
768 |
768 |
769 export_code divmod_integer in Haskell file_prefix divmod |
|
770 |
|
771 |
769 |
772 subsection \<open>Type of target language naturals\<close> |
770 subsection \<open>Type of target language naturals\<close> |
773 |
771 |
774 typedef natural = "UNIV :: nat set" |
772 typedef natural = "UNIV :: nat set" |
775 morphisms nat_of_natural natural_of_nat .. |
773 morphisms nat_of_natural natural_of_nat .. |