# HG changeset patch # User haftmann # Date 1240590037 -7200 # Node ID b2fa60d5673540fafd70a1f153c1e72caaa79b0f # Parent 415f2fe37f62b5b70c677b84b6e5db6b2ff7c9b6 some jokes are just too bad to appear in a theory file diff -r 415f2fe37f62 -r b2fa60d56735 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Apr 24 18:01:39 2009 +0200 +++ b/src/HOL/Nat.thy Fri Apr 24 18:20:37 2009 +0200 @@ -1206,7 +1206,7 @@ "funpow (Suc n) f = f o funpow n f" unfolding funpow_code_def by simp_all -definition "foo = id ^^ (1 + 1)" +hide (open) const funpow lemma funpow_add: "f ^^ (m + n) = f ^^ m \ f ^^ n"