src/HOL/Library/Code_Integer.thy
changeset 25767 852bce03412a
parent 24999 1dbe785ed529
child 25919 8b1c0d434824
     1.1 --- a/src/HOL/Library/Code_Integer.thy	Wed Jan 02 15:14:22 2008 +0100
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Wed Jan 02 15:14:23 2008 +0100
     1.3 @@ -88,10 +88,10 @@
     1.4    (OCaml "Big'_int.lt'_big'_int")
     1.5    (Haskell infix 4 "<")
     1.6  
     1.7 -code_const index_of_int and int_of_index
     1.8 +(*code_const index_of_int and int_of_index
     1.9    (SML "IntInf.toInt" and "IntInf.fromInt")
    1.10    (OCaml "Big'_int.int'_of'_big'_int" and "Big'_int.big'_int'_of'_int")
    1.11 -  (Haskell "_" and "_")
    1.12 +  (Haskell "_" and "_") FIXME perhaps recover this if neccessary *)
    1.13  
    1.14  code_reserved SML IntInf
    1.15  code_reserved OCaml Big_int