1.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Sat Jul 09 19:28:33 2011 +0200
     1.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Sat Jul 09 19:29:25 2011 +0200
     1.3 @@ -294,6 +294,29 @@
     1.4  quickcheck[random, size = 10]
     1.5  oops
     1.6  
     1.7 +subsubsection {* floor and ceiling functions *}
     1.8 +
     1.9 +lemma
    1.10 +  "floor x + floor y = floor (x + y :: rat)"
    1.11 +quickcheck[expect = counterexample]
    1.12 +oops
    1.13 +
    1.14 +lemma
    1.15 +  "floor x + floor y = floor (x + y :: real)"
    1.16 +quickcheck[expect = counterexample]
    1.17 +oops
    1.18 +
    1.19 +lemma
    1.20 +  "ceiling x + ceiling y = ceiling (x + y :: rat)"
    1.21 +quickcheck[expect = counterexample]
    1.22 +oops
    1.23 +
    1.24 +lemma
    1.25 +  "ceiling x + ceiling y = ceiling (x + y :: real)"
    1.26 +quickcheck[expect = counterexample]
    1.27 +oops
    1.28 +
    1.29 +
    1.30  subsection {* Examples with Records *}
    1.31  
    1.32  record point =