--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Sat Oct 01 12:03:27 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Sat Oct 01 17:16:35 2016 +0200
@@ -99,7 +99,7 @@
(auto intro!: mono_funpow sup_continuous_mono[OF f] SUP_least)
show "lfp g \<le> \<alpha> (lfp f)"
- by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_unfold[OF mf, symmetric])
+ by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_fixpoint[OF mf])
qed
lemma sup_continuous_applyD: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x h)"