# HG changeset patch
# User wenzelm
# Date 1551898082 -3600
# Node ID bb16c0bb7520d4a39c291bd5961ff0ab76a91cbc
# Parent  02e0458d342f9710a67ae570f467007e6411c1a9
removed junk;

diff -r 02e0458d342f -r bb16c0bb7520 src/HOL/Library/Order_Continuity.thy
--- 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)"