diff -r 00db2eed7189 -r 2dee03f192b7 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Jun 10 15:03:29 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Jun 10 15:42:21 2011 +0200
@@ -10,27 +10,29 @@
 begin
 
 subsection {* Minimalistic examples *}
-(*
+
 lemma
   "x = y"
 quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
 oops
-*)
-(*
+
 lemma
   "x = y"
-quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
+quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
 oops
-*)
 
-(*declare [[quickcheck_narrowing_overlord]]*)
 subsection {* Simple examples with existentials *}
 
 lemma
   "\<exists> y :: nat. \<forall> x. x = y"
 quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
 oops
-
+(*
+lemma
+  "\<exists> y :: int. \<forall> x. x = y"
+quickcheck[tester = narrowing, size = 2]
+oops
+*)
 lemma
   "x > 1 --> (\<exists>y :: nat. x < y & y <= 1)"
 quickcheck[tester = narrowing, finite_types = false, expect = counterexample]