src/HOL/Nat.thy
changeset 62217 527488dc8b90
parent 61799 4cf66f21b764
child 62326 3cf7a067599c
     1.1 --- a/src/HOL/Nat.thy	Wed Jan 20 20:19:05 2016 +0100
     1.2 +++ b/src/HOL/Nat.thy	Fri Jan 22 16:00:03 2016 +0000
     1.3 @@ -1329,6 +1329,9 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma funpow_0 [simp]: "(f ^^ 0) x = x"
     1.8 +  by simp
     1.9 +
    1.10  lemma funpow_Suc_right:
    1.11    "f ^^ Suc n = f ^^ n \<circ> f"
    1.12  proof (induct n)