src/HOL/Library/Extended_Nat.thy
changeset 69861 62e47f06d22c
parent 69803 a24865b6262f
--- a/src/HOL/Library/Extended_Nat.thy	Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Tue Mar 05 07:00:21 2019 +0000
@@ -678,7 +678,8 @@
   by(auto simp add: Sup_enat_def eSuc_Max inj_on_def dest: finite_imageD)
 
 lemma sup_continuous_eSuc: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. eSuc (f x))"
-  using  eSuc_Sup[of "_ ` UNIV"] by (auto simp: sup_continuous_def)
+  using eSuc_Sup [of "_ ` UNIV"] by (auto simp: sup_continuous_def image_comp)
+
 
 subsection \<open>Traditional theorem names\<close>