diff -r cf5e008d38c4 -r 2e901158675e src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Fri Dec 17 08:37:35 2010 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Fri Dec 17 12:14:18 2010 +0100
@@ -6,7 +6,7 @@
 header {* Examples for the 'quickcheck' command *}
 
 theory Quickcheck_Examples
-imports Main
+imports Complex_Main
 begin
 
 text {*
@@ -237,7 +237,7 @@
 quickcheck[exhaustive, expect = counterexample]
 oops
 
-section {* Examples with quantifiers *}
+subsection {* Examples with quantifiers *}
 
 text {*
   These examples show that we can handle quantifiers.
@@ -258,4 +258,34 @@
   quickcheck[expect = counterexample]
 oops
 
+subsection {* Examples with numerical types *}
+
+text {*
+Quickcheck supports the common types nat, int, rat and real.
+*}
+
+lemma
+  "(x :: nat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
+quickcheck[exhaustive, size = 10, expect = counterexample]
+quickcheck[random, size = 10]
+oops
+
+lemma
+  "(x :: int) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
+quickcheck[exhaustive, size = 10, expect = counterexample]
+quickcheck[random, size = 10]
+oops
+
+lemma
+  "(x :: rat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
+quickcheck[exhaustive, size = 10, expect = counterexample]
+quickcheck[random, size = 10]
+oops
+
+lemma
+  "(x :: real) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
+quickcheck[exhaustive, size = 10, expect = counterexample]
+quickcheck[random, size = 10]
+oops
+
 end