Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nat.thy
changeset 30975 b2fa60d56735
parent 30971 7fbebf75b3ef
child 31024 0fdf666e08bf 
--- 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"
isabelle