author | haftmann |
Fri, 24 Apr 2009 18:20:37 +0200 | |
changeset 30975 | b2fa60d56735 |
parent 30974 | 415f2fe37f62 |
child 30976 | 44637646fa17 |
src/HOL/Nat.thy | file | annotate | diff | comparison | revisions |
--- 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 \<circ> f ^^ n"