# HG changeset patch
# User bulwahn
# Date 1322644052 -3600
# Node ID 4c25ba9f3c23a1daac4ed4e5c5bc21a99f36a8f0
# Parent  d4ac5e090cd94095586c81ee781cd9f0b6c23074
adding examples for the potential counterexamples in the simple scheme

diff -r d4ac5e090cd9 -r 4c25ba9f3c23 src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Wed Nov 30 09:35:58 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Wed Nov 30 10:07:32 2011 +0100
@@ -426,5 +426,28 @@
 quickcheck[exhaustive, potential = true, expect = counterexample]
 oops
 
+text {* with the simple testing scheme *}
+
+setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
+declare [[quickcheck_full_support = false]]
+
+lemma
+  "xs = [] ==> hd xs \<noteq> x"
+quickcheck[exhaustive, potential = false, expect = no_counterexample]
+quickcheck[exhaustive, potential = true, expect = counterexample]
+oops
+
+lemma
+  "xs = [] ==> hd xs = x"
+quickcheck[exhaustive, potential = false, expect = no_counterexample]
+quickcheck[exhaustive, potential = true, expect = counterexample]
+oops
+
+lemma "xs = [] ==> hd xs = x ==> x = y"
+quickcheck[exhaustive, potential = false, expect = no_counterexample]
+quickcheck[exhaustive, potential = true, expect = counterexample]
+oops
+
+declare [[quickcheck_full_support = true]]
 
 end