# HG changeset patch
# User bulwahn
# Date 1304585253 -7200
# Node ID 7c7ca3fc7ce53fee147f25c4acd4528eeb200ab7
# Parent  a94ad372b2f578dec79c5ee5f1ac9eb6ef0a4340
adding examples for invoking quickcheck with records

diff -r a94ad372b2f5 -r 7c7ca3fc7ce5 src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Thu May 05 10:47:31 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Thu May 05 10:47:33 2011 +0200
@@ -294,6 +294,29 @@
 quickcheck[random, size = 10]
 oops
 
+subsection {* Examples with Records *}
+
+record point =
+  xpos :: nat
+  ypos :: nat
+
+lemma
+  "xpos r = xpos r' ==> r = r'"
+quickcheck[exhaustive, expect = counterexample]
+quickcheck[random, expect = counterexample]
+oops
+
+datatype colour = Red | Green | Blue
+
+record cpoint = point +
+  colour :: colour
+
+lemma
+  "xpos r = xpos r' ==> ypos r = ypos r' ==> (r :: cpoint) = r'"
+quickcheck[exhaustive, expect = counterexample]
+quickcheck[random, expect = counterexample]
+oops
+
 subsection {* Examples with locales *}
 
 locale Truth