1.1 --- a/src/HOL/Nat.thy	Tue Feb 09 11:07:14 2010 +0100
     1.2 +++ b/src/HOL/Nat.thy	Tue Feb 09 11:47:47 2010 +0100
     1.3 @@ -176,7 +176,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -hide (open) fact add_0_right
     1.8 +hide (open) fact add_0 add_0_right diff_0
     1.9  
    1.10  instantiation nat :: comm_semiring_1_cancel
    1.11  begin
    1.12 @@ -1491,6 +1491,8 @@
    1.13  lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
    1.14  by (simp split add: nat_diff_split)
    1.15  
    1.16 +hide (open) fact diff_diff_eq
    1.17 +
    1.18  lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
    1.19  by (auto split add: nat_diff_split)
    1.20  

     2.1 --- a/src/HOL/Tools/Function/size.ML	Tue Feb 09 11:07:14 2010 +0100
     2.2 +++ b/src/HOL/Tools/Function/size.ML	Tue Feb 09 11:47:47 2010 +0100
     2.3 @@ -153,7 +153,7 @@
     2.4  
     2.5      val ctxt = ProofContext.init thy';
     2.6  
     2.7 -    val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm Nat.add_0_right} ::
     2.8 +    val simpset1 = HOL_basic_ss addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
     2.9        size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
    2.10      val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
    2.11  

     3.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Feb 09 11:07:14 2010 +0100
     3.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Feb 09 11:47:47 2010 +0100
     3.3 @@ -60,7 +60,7 @@
     3.4    (Simplifier.rewrite 
     3.5      (HOL_basic_ss 
     3.6         addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
     3.7 -             @ [if_False, if_True, @{thm add_0}, @{thm add_Suc},
     3.8 +             @ [if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc},
     3.9                   @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
    3.10               @ map (fn th => th RS sym) @{thms numerals}));
    3.11  
    3.12 @@ -634,7 +634,7 @@
    3.13  
    3.14  val nat_arith = @{thms "nat_arith"};
    3.15  val nat_exp_ss = HOL_basic_ss addsimps (@{thms nat_number} @ nat_arith @ @{thms arith_simps} @ @{thms rel_simps})
    3.16 -                              addsimps [Let_def, if_False, if_True, @{thm add_0}, @{thm add_Suc}];
    3.17 +                              addsimps [Let_def, if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc}];
    3.18  
    3.19  fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
    3.20  

     4.1 --- a/src/HOL/Tools/nat_arith.ML	Tue Feb 09 11:07:14 2010 +0100
     4.2 +++ b/src/HOL/Tools/nat_arith.ML	Tue Feb 09 11:47:47 2010 +0100
     4.3 @@ -51,7 +51,7 @@
     4.4    val dest_sum = dest_sum;
     4.5    val prove_conv = Arith_Data.prove_conv2;
     4.6    val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
     4.7 -    @{thm add_0}, @{thm Nat.add_0_right}];
     4.8 +    @{thm Nat.add_0}, @{thm Nat.add_0_right}];
     4.9    val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
    4.10    fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    4.11    fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}

     5.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Feb 09 11:07:14 2010 +0100
     5.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Feb 09 11:47:47 2010 +0100
     5.3 @@ -124,7 +124,7 @@
     5.4  
     5.5  
     5.6  (*Simplify 1*n and n*1 to n*)
     5.7 -val add_0s  = map rename_numerals [@{thm add_0}, @{thm Nat.add_0_right}];
     5.8 +val add_0s  = map rename_numerals [@{thm Nat.add_0}, @{thm Nat.add_0_right}];
     5.9  val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
    5.10  
    5.11  (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
    5.12 @@ -136,7 +136,7 @@
    5.13  
    5.14  val simplify_meta_eq =
    5.15      Arith_Data.simplify_meta_eq
    5.16 -        ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm Nat.add_0_right},
    5.17 +        ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm Nat.add_0}, @{thm Nat.add_0_right},
    5.18            @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
    5.19  
    5.20  

     6.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Tue Feb 09 11:07:14 2010 +0100
     6.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Tue Feb 09 11:47:47 2010 +0100
     6.3 @@ -373,7 +373,7 @@
     6.4      [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}] @ simps
     6.5    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
     6.6    val simplify_meta_eq = Arith_Data.simplify_meta_eq
     6.7 -    [@{thm add_0}, @{thm Nat.add_0_right}, @{thm mult_zero_left},
     6.8 +    [@{thm Nat.add_0}, @{thm Nat.add_0_right}, @{thm mult_zero_left},
     6.9        @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
    6.10    end
    6.11