src/HOL/Nat.thy

   show "0 + n = n" by simp
 qed
 
 end
 
-hide (open) fact add_0_right
+hide (open) fact add_0 add_0_right diff_0
 
 instantiation nat :: comm_semiring_1_cancel
 begin
 
 definition

 text {* Simplification of relational expressions involving subtraction *}
 
 lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
 by (simp split add: nat_diff_split)
 
+hide (open) fact diff_diff_eq
+
 lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
 by (auto split add: nat_diff_split)
 
 lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
 by (auto split add: nat_diff_split)