src/HOL/Nat.thy
changeset 30975 b2fa60d56735
parent 30971 7fbebf75b3ef
child 31024 0fdf666e08bf
     1.1 --- a/src/HOL/Nat.thy	Fri Apr 24 18:01:39 2009 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Apr 24 18:20:37 2009 +0200
     1.3 @@ -1206,7 +1206,7 @@
     1.4    "funpow (Suc n) f = f o funpow n f"
     1.5    unfolding funpow_code_def by simp_all
     1.6  
     1.7 -definition "foo = id ^^ (1 + 1)"
     1.8 +hide (open) const funpow
     1.9  
    1.10  lemma funpow_add:
    1.11    "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"