1.1 --- a/src/HOL/Nat.thy	Mon Feb 08 17:12:24 2010 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Feb 08 17:12:27 2010 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Natural numbers *}
     1.5  
     1.6  theory Nat
     1.7 -imports Inductive Product_Type Ring_and_Field
     1.8 +imports Inductive Product_Type Fields
     1.9  uses
    1.10    "~~/src/Tools/rat.ML"
    1.11    "~~/src/Provers/Arith/cancel_sums.ML"
    1.12 @@ -176,6 +176,8 @@
    1.13  
    1.14  end
    1.15  
    1.16 +hide (open) fact add_0_right
    1.17 +
    1.18  instantiation nat :: comm_semiring_1_cancel
    1.19  begin
    1.20  
    1.21 @@ -730,7 +732,7 @@
    1.22    apply (induct n)
    1.23    apply (simp_all add: order_le_less)
    1.24    apply (blast elim!: less_SucE
    1.25 -               intro!: add_0_right [symmetric] add_Suc_right [symmetric])
    1.26 +               intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric])
    1.27    done
    1.28  
    1.29  text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}

     2.1 --- a/src/HOL/Nat_Numeral.thy	Mon Feb 08 17:12:24 2010 +0100
     2.2 +++ b/src/HOL/Nat_Numeral.thy	Mon Feb 08 17:12:27 2010 +0100
     2.3 @@ -64,7 +64,7 @@
     2.4  
     2.5  lemma power_even_eq:
     2.6    "a ^ (2*n) = (a ^ n) ^ 2"
     2.7 -  by (subst OrderedGroup.mult_commute) (simp add: power_mult)
     2.8 +  by (subst mult_commute) (simp add: power_mult)
     2.9  
    2.10  lemma power_odd_eq:
    2.11    "a ^ Suc (2*n) = a * (a ^ n) ^ 2"

     3.1 --- a/src/HOL/Tools/Function/size.ML	Mon Feb 08 17:12:24 2010 +0100
     3.2 +++ b/src/HOL/Tools/Function/size.ML	Mon Feb 08 17:12:27 2010 +0100
     3.3 @@ -153,7 +153,7 @@
     3.4  
     3.5      val ctxt = ProofContext.init thy';
     3.6  
     3.7 -    val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm add_0_right} ::
     3.8 +    val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm Nat.add_0_right} ::
     3.9        size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
    3.10      val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
    3.11  

     4.1 --- a/src/HOL/Tools/nat_arith.ML	Mon Feb 08 17:12:24 2010 +0100
     4.2 +++ b/src/HOL/Tools/nat_arith.ML	Mon Feb 08 17:12:27 2010 +0100
     4.3 @@ -50,8 +50,8 @@
     4.4    val mk_sum = mk_norm_sum;
     4.5    val dest_sum = dest_sum;
     4.6    val prove_conv = Arith_Data.prove_conv2;
     4.7 -  val norm_tac1 = Arith_Data.simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
     4.8 -    @{thm "add_0"}, @{thm "add_0_right"}];
     4.9 +  val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
    4.10 +    @{thm add_0}, @{thm Nat.add_0_right}];
    4.11    val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
    4.12    fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    4.13    fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}