src/HOL/Nat.thy
changeset 36176 3fe7e97ccca8
parent 35828 46cfc4b8112e
child 36977 71c8973a604b
     1.1 --- a/src/HOL/Nat.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -hide (open) fact add_0 add_0_right diff_0
     1.8 +hide_fact (open) add_0 add_0_right diff_0
     1.9  
    1.10  instantiation nat :: comm_semiring_1_cancel
    1.11  begin
    1.12 @@ -1212,7 +1212,7 @@
    1.13    "funpow (Suc n) f = f o funpow n f"
    1.14    unfolding funpow_code_def by simp_all
    1.15  
    1.16 -hide (open) const funpow
    1.17 +hide_const (open) funpow
    1.18  
    1.19  lemma funpow_add:
    1.20    "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
    1.21 @@ -1504,7 +1504,7 @@
    1.22  lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
    1.23  by (simp split add: nat_diff_split)
    1.24  
    1.25 -hide (open) fact diff_diff_eq
    1.26 +hide_fact (open) diff_diff_eq
    1.27  
    1.28  lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
    1.29  by (auto split add: nat_diff_split)