Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed junk;
authorwenzelm
Wed, 06 Mar 2019 19:48:02 +0100
changeset 69872 bb16c0bb7520
parent 69871 02e0458d342f
child 69873 6ebe97815275
removed junk;
src/HOL/Library/Order_Continuity.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle