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/Quickcheck_Examples/Quickcheck_Examples.thy
changeset 63882 018998c00003
parent 63167 0909deb8059b
child 63901 4ce989e962e0 
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Thu Sep 15 11:48:20 2016 +0200
@@ -204,7 +204,7 @@
 oops
 
 lemma
-  "ns ! k < length ns ==> k <= listsum ns"
+  "ns ! k < length ns ==> k <= sum_list ns"
 quickcheck[random, iterations = 10000, finite_types = false, quiet]
 quickcheck[exhaustive, finite_types = false, expect = counterexample]
 oops
isabelle