src/HOL/Nat.thy
changeset 63979 95c3ae4baba8
parent 63648 f9f3006a5579
child 64447 e44f5c123f26
     1.1 --- a/src/HOL/Nat.thy	Sat Oct 01 12:03:27 2016 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sat Oct 01 17:16:35 2016 +0200
     1.3 @@ -1554,7 +1554,7 @@
     1.4        by (simp add: comp_def)
     1.5    qed
     1.6    have "(f ^^ n) (lfp f) = lfp f" for n
     1.7 -    by (induct n) (auto intro: f lfp_unfold[symmetric])
     1.8 +    by (induct n) (auto intro: f lfp_fixpoint)
     1.9    then show "lfp (f ^^ Suc n) \<le> lfp f"
    1.10      by (intro lfp_lowerbound) (simp del: funpow.simps)
    1.11  qed
    1.12 @@ -1571,7 +1571,7 @@
    1.13        by (simp add: comp_def)
    1.14    qed
    1.15    have "(f ^^ n) (gfp f) = gfp f" for n
    1.16 -    by (induct n) (auto intro: f gfp_unfold[symmetric])
    1.17 +    by (induct n) (auto intro: f gfp_fixpoint)
    1.18    then show "gfp (f ^^ Suc n) \<ge> gfp f"
    1.19      by (intro gfp_upperbound) (simp del: funpow.simps)
    1.20  qed