src/HOL/IMP/Denotational.thy

--- a/src/HOL/IMP/Denotational.thy	Wed Jan 20 20:19:05 2016 +0100
+++ b/src/HOL/IMP/Denotational.thy	Fri Jan 22 16:00:03 2016 +0000
@@ -105,7 +105,7 @@
       by(simp add: cont_def)
     also have "\<dots> = (f^^0){} \<union> \<dots>" by simp
     also have "\<dots> = ?U"
-      by(auto simp del: funpow.simps) (metis not0_implies_Suc)
+      using assms funpow_decreasing le_SucI mono_if_cont by blast
     finally show "f ?U \<subseteq> ?U" by simp
   qed
 next