src/HOL/Library/Code_Target_Int.thy
changeset 51143 0a2371e7ced3
parent 51114 3e913a575dc6
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/Library/Code_Target_Int.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Implementation of integer numbers by target-language integers *}
     1.5  
     1.6  theory Code_Target_Int
     1.7 -imports Main "~~/src/HOL/Library/Code_Numeral_Types"
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  code_datatype int_of_integer
    1.12 @@ -54,7 +54,7 @@
    1.13    by transfer simp
    1.14  
    1.15  lemma [code]:
    1.16 -  "Int.dup k = int_of_integer (Code_Numeral_Types.dup (of_int k))"
    1.17 +  "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
    1.18    by transfer simp
    1.19  
    1.20  lemma [code, code del]:
    1.21 @@ -66,7 +66,7 @@
    1.22  
    1.23  lemma [code]:
    1.24    "pdivmod k l = map_pair int_of_integer int_of_integer
    1.25 -    (Code_Numeral_Types.divmod_abs (of_int k) (of_int l))"
    1.26 +    (Code_Numeral.divmod_abs (of_int k) (of_int l))"
    1.27    by (simp add: prod_eq_iff pdivmod_def)
    1.28  
    1.29  lemma [code]: