src/HOL/Library/Code_Integer.thy
changeset 49446 6efff142bb54
parent 49088 1b609a7837ef
equal deleted inserted replaced
49445:6cbfe187a0f9 49446:6efff142bb54
   149   (Eval infixl 6 "<")
   149   (Eval infixl 6 "<")
   150 
   150 
   151 code_const Code_Numeral.int_of
   151 code_const Code_Numeral.int_of
   152   (SML "IntInf.fromInt")
   152   (SML "IntInf.fromInt")
   153   (OCaml "_")
   153   (OCaml "_")
   154   (Haskell "toInteger")
   154   (Haskell "Prelude.toInteger")
   155   (Scala "!_.as'_BigInt")
   155   (Scala "!_.as'_BigInt")
   156   (Eval "_")
   156   (Eval "_")
   157 
   157 
   158 code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term"
   158 code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term"
   159   (Eval "HOLogic.mk'_number/ HOLogic.intT")
   159   (Eval "HOLogic.mk'_number/ HOLogic.intT")