src/HOL/Code_Numeral.thy
changeset 69593 3dda49e08b9d
parent 68028 1f9f973eed2a
child 69906 55534affe445
equal deleted inserted replaced
69592:a80d8ec6c998 69593:3dda49e08b9d
   666     and (Haskell) "!(0/ ::/ Integer)"
   666     and (Haskell) "!(0/ ::/ Integer)"
   667     and (Scala) "BigInt(0)"
   667     and (Scala) "BigInt(0)"
   668 
   668 
   669 setup \<open>
   669 setup \<open>
   670   fold (fn target =>
   670   fold (fn target =>
   671     Numeral.add_code @{const_name Code_Numeral.Pos} I Code_Printer.literal_numeral target
   671     Numeral.add_code \<^const_name>\<open>Code_Numeral.Pos\<close> I Code_Printer.literal_numeral target
   672     #> Numeral.add_code @{const_name Code_Numeral.Neg} (~) Code_Printer.literal_numeral target)
   672     #> Numeral.add_code \<^const_name>\<open>Code_Numeral.Neg\<close> (~) Code_Printer.literal_numeral target)
   673     ["SML", "OCaml", "Haskell", "Scala"]
   673     ["SML", "OCaml", "Haskell", "Scala"]
   674 \<close>
   674 \<close>
   675 
   675 
   676 code_printing
   676 code_printing
   677   constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   677   constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>