--- 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