src/HOL/Nat.thy
changeset 35064 1bdef0c013d3
parent 35047 1b2bae06c796
child 35121 36c0a6dd8c6f
     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