src/HOL/Code_Numeral.thy
changeset 81706 7beb0cf38292
parent 81681 bac9b067c768
child 81712 97987036f051
equal deleted inserted replaced
81705:53fea2ccab19 81706:7beb0cf38292
   778 hide_const (open) Pos Neg sub dup divmod_abs
   778 hide_const (open) Pos Neg sub dup divmod_abs
   779 
   779 
   780 
   780 
   781 subsection \<open>Serializer setup for target language integers\<close>
   781 subsection \<open>Serializer setup for target language integers\<close>
   782 
   782 
   783 code_reserved Eval int Integer abs
   783 code_reserved
       
   784   (Eval) int Integer abs
   784 
   785 
   785 code_printing
   786 code_printing
   786   type_constructor integer \<rightharpoonup>
   787   type_constructor integer \<rightharpoonup>
   787     (SML) "IntInf.int"
   788     (SML) "IntInf.int"
   788     and (OCaml) "Z.t"
   789     and (OCaml) "Z.t"