# HG changeset patch
# User bulwahn
# Date 1322774075 -3600
# Node ID d8fbd3fa0375c30afc82395294800ffdb330cae5
# Parent  39c52a820f6e50e220d5fda9cfee744e344fe6a7
adding examples for quickcheck-random

diff -r 39c52a820f6e -r d8fbd3fa0375 src/HOL/ex/Quickcheck_Examples.thy
--- 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 *}