Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adding examples for quickcheck-random
authorbulwahn
Thu, 01 Dec 2011 22:14:35 +0100
changeset 45720 d8fbd3fa0375
parent 45719 39c52a820f6e
child 45721 d1fb55c2ed65
adding examples for quickcheck-random
src/HOL/ex/Quickcheck_Examples.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/Quickcheck_Examples.thy	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Thu Dec 01 22:14:35 2011 +0100
@@ -413,17 +413,23 @@
   "xs = [] ==> hd xs \<noteq> x"
 quickcheck[exhaustive, potential = false, expect = no_counterexample]
 quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[random, potential = false, report = false, expect = no_counterexample]
+quickcheck[random, potential = true, report = false, expect = counterexample]
 oops
 
 lemma
   "xs = [] ==> hd xs = x"
 quickcheck[exhaustive, potential = false, expect = no_counterexample]
 quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[random, potential = false, report = false, expect = no_counterexample]
+quickcheck[random, potential = true, report = false, expect = counterexample]
 oops
 
 lemma "xs = [] ==> hd xs = x ==> x = y"
 quickcheck[exhaustive, potential = false, expect = no_counterexample]
 quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[random, potential = false, report = false, expect = no_counterexample]
+quickcheck[random, potential = true, report = false, expect = counterexample]
 oops
 
 text {* with the simple testing scheme *}
isabelle