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/Metis_Examples/Big_O.thy
changeset 57418 6ab1c7cb0b8d
parent 57245 f6bf6d5341ee
child 57512 cc97b347b301 
--- a/src/HOL/Metis_Examples/Big_O.thy	Fri Jun 27 22:08:55 2014 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy	Sat Jun 28 09:16:42 2014 +0200
@@ -552,7 +552,8 @@
  apply (erule ssubst)
  apply (erule bigo_setsum3)
 apply (rule ext)
-apply (rule setsum_cong2)
+apply (rule setsum.cong)
+apply (rule refl)
 by (metis abs_of_nonneg zero_le_mult_iff)
 
 lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
isabelle