--- a/src/HOL/Nat.thy Wed Jan 20 20:19:05 2016 +0100
+++ b/src/HOL/Nat.thy Fri Jan 22 16:00:03 2016 +0000
@@ -1329,6 +1329,9 @@
end
+lemma funpow_0 [simp]: "(f ^^ 0) x = x"
+ by simp
+
lemma funpow_Suc_right:
"f ^^ Suc n = f ^^ n \<circ> f"
proof (induct n)