author | wenzelm |
Wed, 06 Mar 2019 19:48:02 +0100 (2019-03-06) | |
changeset 69872 | bb16c0bb7520 |
parent 69871 | 02e0458d342f |
child 69873 | 6ebe97815275 |
--- a/src/HOL/Library/Order_Continuity.thy Wed Mar 06 19:29:46 2019 +0100 +++ b/src/HOL/Library/Order_Continuity.thy Wed Mar 06 19:48:02 2019 +0100 @@ -51,7 +51,6 @@ by (auto intro: monoI) with \<open>sup_continuous F\<close> have *: "F (SUP i. ?f i) = (SUP i. F (?f i))" by (auto dest: sup_continuousD) - thm this [simplified, simplified SUP_nat_binary] from \<open>A \<le> B\<close> have "B = sup A B" by (simp add: le_iff_sup) then have "F B = F (sup A B)"