some jokes are just too bad to appear in a theory file
authorhaftmann
Fri Apr 24 18:20:37 2009 +0200 (2009-04-24)
changeset 30975b2fa60d56735
parent 30974 415f2fe37f62
child 30976 44637646fa17
some jokes are just too bad to appear in a theory file
src/HOL/Nat.thy
     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"