--- a/src/HOL/ex/Quickcheck_Examples.thy Fri Jan 27 10:31:30 2012 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Fri Jan 27 10:31:31 2012 +0100
@@ -414,7 +414,7 @@
begin
lemma "False"
-quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[exhaustive, expect = counterexample]
oops
end
@@ -430,6 +430,19 @@
end
+locale antisym =
+ fixes R
+ assumes "R x y --> R y x --> x = y"
+begin
+
+lemma
+ "R x y --> R y z --> R x z"
+quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+end
+
subsection {* Examples with HOL quantifiers *}
lemma