src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
changeset 63882 018998c00003
parent 63167 0909deb8059b
child 63901 4ce989e962e0
     1.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Sep 14 22:07:11 2016 +0200
     1.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Thu Sep 15 11:48:20 2016 +0200
     1.3 @@ -204,7 +204,7 @@
     1.4  oops
     1.5  
     1.6  lemma
     1.7 -  "ns ! k < length ns ==> k <= listsum ns"
     1.8 +  "ns ! k < length ns ==> k <= sum_list ns"
     1.9  quickcheck[random, iterations = 10000, finite_types = false, quiet]
    1.10  quickcheck[exhaustive, finite_types = false, expect = counterexample]
    1.11  oops