--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Fri Mar 18 18:19:42 2011 +0100
@@ -10,12 +10,12 @@
begin
subsection {* Minimalistic examples *}
-
+(*
lemma
"x = y"
-quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
+quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
oops
-
+*)
(*
lemma
"x = y"
@@ -30,6 +30,10 @@
oops
lemma "rev xs = xs"
+ quickcheck[tester = narrowing, finite_types = false, default_type = int]
+oops
+
+lemma "rev xs = xs"
quickcheck[tester = narrowing, finite_types = true]
oops