Mercurial Mercurial > hg > lexing / 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.
thys2/ClosedFormsBounds.thy
changeset 480 574749f5190b
parent 454 3938480e17f7
child 492 61eff2abb0b6 
--- a/thys2/ClosedFormsBounds.thy	Mon Apr 04 23:56:40 2022 +0100
+++ b/thys2/ClosedFormsBounds.thy	Thu Apr 07 21:31:29 2022 +0100
@@ -208,7 +208,7 @@
                    \<le>  (sum_list
                     (map rsize (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))")
   apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15))
-  apply (metis (no_types, opaque_lifting) add_Suc_right le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
+  apply (metis (no_types, opaque_lifting)  le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
             apply fastforce
            apply fastforce
   apply (metis Un_iff insert_absorb)
lexing