1.1 --- a/src/HOL/Library/Target_Numeral.thy	Sat Apr 28 07:38:22 2012 +0200
     1.2 +++ b/src/HOL/Library/Target_Numeral.thy	Sat Apr 28 09:55:01 2012 +0200
     1.3 @@ -657,30 +657,30 @@
     1.4    by (simp add: Target_Numeral.int_eq_iff)
     1.5  
     1.6  lemma [code abstract]:
     1.7 -  "Target_Numeral.of_nat (m + n) = of_nat m + of_nat n"
     1.8 +  "Target_Numeral.of_nat (m + n) = Target_Numeral.of_nat m + Target_Numeral.of_nat n"
     1.9    by (simp add: Target_Numeral.int_eq_iff)
    1.10  
    1.11  lemma [code abstract]:
    1.12 -  "Target_Numeral.of_nat (Code_Nat.dup n) = Target_Numeral.dup (of_nat n)"
    1.13 +  "Target_Numeral.of_nat (Code_Nat.dup n) = Target_Numeral.dup (Target_Numeral.of_nat n)"
    1.14    by (simp add: Target_Numeral.int_eq_iff Code_Nat.dup_def)
    1.15  
    1.16  lemma [code, code del]:
    1.17    "Code_Nat.sub = Code_Nat.sub" ..
    1.18  
    1.19  lemma [code abstract]:
    1.20 -  "Target_Numeral.of_nat (m - n) = max 0 (of_nat m - of_nat n)"
    1.21 +  "Target_Numeral.of_nat (m - n) = max 0 (Target_Numeral.of_nat m - Target_Numeral.of_nat n)"
    1.22    by (simp add: Target_Numeral.int_eq_iff)
    1.23  
    1.24  lemma [code abstract]:
    1.25 -  "Target_Numeral.of_nat (m * n) = of_nat m * of_nat n"
    1.26 +  "Target_Numeral.of_nat (m * n) = Target_Numeral.of_nat m * Target_Numeral.of_nat n"
    1.27    by (simp add: Target_Numeral.int_eq_iff of_nat_mult)
    1.28  
    1.29  lemma [code abstract]:
    1.30 -  "Target_Numeral.of_nat (m div n) = of_nat m div of_nat n"
    1.31 +  "Target_Numeral.of_nat (m div n) = Target_Numeral.of_nat m div Target_Numeral.of_nat n"
    1.32    by (simp add: Target_Numeral.int_eq_iff zdiv_int)
    1.33  
    1.34  lemma [code abstract]:
    1.35 -  "Target_Numeral.of_nat (m mod n) = of_nat m mod of_nat n"
    1.36 +  "Target_Numeral.of_nat (m mod n) = Target_Numeral.of_nat m mod Target_Numeral.of_nat n"
    1.37    by (simp add: Target_Numeral.int_eq_iff zmod_int)
    1.38  
    1.39  lemma [code]:
    1.40 @@ -735,3 +735,4 @@
    1.41    by (simp add: of_nat_def of_int_of_nat max_def)
    1.42  
    1.43  end
    1.44 +