1.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Mon Oct 03 14:43:14 2011 +0200
     1.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Mon Oct 03 14:43:15 2011 +0200
     1.3 @@ -266,6 +266,20 @@
     1.4    quickcheck[expect = counterexample]
     1.5  oops
     1.6  
     1.7 +
     1.8 +subsection {* Examples with relations *}
     1.9 +
    1.10 +lemma
    1.11 +  "acyclic R ==> acyclic S ==> acyclic (R Un S)"
    1.12 +quickcheck[expect = counterexample]
    1.13 +oops
    1.14 +
    1.15 +lemma
    1.16 +  "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
    1.17 +quickcheck[expect = counterexample]
    1.18 +oops
    1.19 +
    1.20 +
    1.21  subsection {* Examples with numerical types *}
    1.22  
    1.23  text {*