src/HOL/Library/Code_Integer.thy
changeset 34944 970e1466028d
parent 34899 8674bb6f727b
child 37947 844977c7abeb
     1.1 --- a/src/HOL/Library/Code_Integer.thy	Fri Jan 22 13:38:28 2010 +0100
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Fri Jan 22 13:38:28 2010 +0100
     1.3 @@ -25,9 +25,9 @@
     1.4  
     1.5  setup {*
     1.6    fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
     1.7 -    true true Code_Printer.str) ["SML", "OCaml", "Haskell", "Scala"]
     1.8 +    true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
     1.9    #> Numeral.add_code @{const_name number_int_inst.number_of_int}
    1.10 -    true true (fn s => (Pretty.block o map Code_Printer.str) ["BigInt", s]) "Scala"
    1.11 +    true Code_Printer.literal_numeral "Scala"
    1.12  *}
    1.13  
    1.14  code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
    1.15 @@ -88,7 +88,7 @@
    1.16  code_const pdivmod
    1.17    (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
    1.18    (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
    1.19 -  (Haskell "divMod/ (abs _)/ (abs _))")
    1.20 +  (Haskell "divMod/ (abs _)/ (abs _)")
    1.21    (Scala "!(_.abs '/% _.abs)")
    1.22  
    1.23  code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    1.24 @@ -113,10 +113,7 @@
    1.25    (SML "IntInf.fromInt")
    1.26    (OCaml "_")
    1.27    (Haskell "toEnum")
    1.28 -  (Scala "!BigInt(_)")
    1.29 -
    1.30 -code_reserved SML IntInf
    1.31 -code_reserved Scala BigInt
    1.32 +  (Scala "!BigInt((_))")
    1.33  
    1.34  text {* Evaluation *}
    1.35