removed junk;
authorwenzelm
Wed Mar 06 19:48:02 2019 +0100 (3 months ago ago)
changeset 70053bb16c0bb7520
parent 70052 02e0458d342f
child 70054 6ebe97815275
removed junk;
src/HOL/Library/Order_Continuity.thy
     1.1 --- a/src/HOL/Library/Order_Continuity.thy	Wed Mar 06 19:29:46 2019 +0100
     1.2 +++ b/src/HOL/Library/Order_Continuity.thy	Wed Mar 06 19:48:02 2019 +0100
     1.3 @@ -51,7 +51,6 @@
     1.4      by (auto intro: monoI)
     1.5    with \<open>sup_continuous F\<close> have *: "F (SUP i. ?f i) = (SUP i. F (?f i))"
     1.6      by (auto dest: sup_continuousD)
     1.7 -  thm this [simplified, simplified SUP_nat_binary]
     1.8    from \<open>A \<le> B\<close> have "B = sup A B"
     1.9      by (simp add: le_iff_sup)
    1.10    then have "F B = F (sup A B)"