Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Extended_Real.thy
changeset 73932 fd21b4a93043
parent 72236 11b81cd70633
child 74325 8d0c2d74ad63 
--- a/src/HOL/Library/Extended_Real.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -1887,7 +1887,7 @@
   subgoal
     by (metis dual_order.strict_trans greaterThanLessThan_iff greaterThan_iff gt_ex not_le order_refl)
   subgoal
-    by (metis (no_types, hide_lams) greaterThanLessThan_empty_iff greaterThanLessThan_iff gt_ex
+    by (metis (no_types, opaque_lifting) greaterThanLessThan_empty_iff greaterThanLessThan_iff gt_ex
         lessThan_iff minus_minus neg_less_iff_less not_less order_less_irrefl)
   subgoal by force
   subgoal
isabelle