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/Series.thy
changeset 73932 fd21b4a93043
parent 73005 83b114a6545f
child 73933 fa92bc604c59 
--- a/src/HOL/Series.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Series.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -713,7 +713,7 @@
     proof (cases m n rule: linorder_class.le_cases)
       assume "m \<le> n"
       then show ?thesis
-        by (metis (mono_tags, hide_lams) M atLeast0LessThan order_trans sum_diff_nat_ivl that zero_le)
+        by (metis (mono_tags, opaque_lifting) M atLeast0LessThan order_trans sum_diff_nat_ivl that zero_le)
     next
       assume "n \<le> m"
       then show ?thesis
isabelle