src/HOL/Library/Code_Integer.thy
changeset 25919 8b1c0d434824
parent 25767 852bce03412a
child 25928 042e877d9841
--- a/src/HOL/Library/Code_Integer.thy	Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Tue Jan 15 16:19:23 2008 +0100
@@ -6,7 +6,7 @@
 header {* Pretty integer literals for code generation *}
 
 theory Code_Integer
-imports IntArith Code_Index
+imports Int
 begin
 
 text {*
@@ -26,13 +26,13 @@
 setup {*
   fold (fn target => CodeTarget.add_pretty_numeral target true
     @{const_name number_int_inst.number_of_int}
-    @{const_name Numeral.B0} @{const_name Numeral.B1}
-    @{const_name Numeral.Pls} @{const_name Numeral.Min}
-    @{const_name Numeral.Bit}
+    @{const_name Int.B0} @{const_name Int.B1}
+    @{const_name Int.Pls} @{const_name Int.Min}
+    @{const_name Int.Bit}
   ) ["SML", "OCaml", "Haskell"]
 *}
 
-code_const "Numeral.Pls" and "Numeral.Min" and "Numeral.Bit"
+code_const "Int.Pls" and "Int.Min" and "Int.Bit"
   (SML "raise/ Fail/ \"Pls\""
      and "raise/ Fail/ \"Min\""
      and "!((_);/ (_);/ raise/ Fail/ \"Bit\")")
@@ -43,12 +43,12 @@
      and "error/ \"Min\""
      and "error/ \"Bit\"")
 
-code_const Numeral.pred
+code_const Int.pred
   (SML "IntInf.- ((_), 1)")
   (OCaml "Big'_int.pred'_big'_int")
   (Haskell "!(_/ -/ 1)")
 
-code_const Numeral.succ
+code_const Int.succ
   (SML "IntInf.+ ((_), 1)")
   (OCaml "Big'_int.succ'_big'_int")
   (Haskell "!(_/ +/ 1)")
@@ -88,11 +88,6 @@
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
 
-(*code_const index_of_int and int_of_index
-  (SML "IntInf.toInt" and "IntInf.fromInt")
-  (OCaml "Big'_int.int'_of'_big'_int" and "Big'_int.big'_int'_of'_int")
-  (Haskell "_" and "_") FIXME perhaps recover this if neccessary *)
-
 code_reserved SML IntInf
 code_reserved OCaml Big_int