# HG changeset patch
# User bulwahn
# Date 1327656691 -3600
# Node ID b6fbdd3d0915d870309763790646b1d33bf785d5
# Parent  6d9535e5291540d0618a64c189b684be4789b6e0
corrected expectation; added an example for quickcheck

diff -r 6d9535e52915 -r b6fbdd3d0915 src/HOL/ex/Quickcheck_Examples.thy
--- 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