diff -r a9445d87bc3e -r 2da02764d523 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- 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
@@ -9,19 +9,31 @@
 imports "~~/src/HOL/Library/Quickcheck_Narrowing"
 begin
 
-subsection {* Simple list examples *}
+subsection {* Minimalistic examples *}
 
-lemma "rev xs = xs"
+lemma
+  "x = y"
 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
 oops
 
-text {* Example fails due to some strange thing... *}
 (*
-lemma "rev xs = xs"
-quickcheck[tester = lazy_exhaustive, finite_types = true]
+lemma
+  "x = y"
+quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
 oops
 *)
 
+subsection {* Simple list examples *}
+
+lemma "rev xs = xs"
+  quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
+oops
+
+lemma "rev xs = xs"
+  quickcheck[tester = narrowing, finite_types = true]
+oops
+
+
 subsection {* AVL Trees *}
 
 datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
@@ -117,7 +129,7 @@
 
 lemma is_ord_l_bal:
  "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"
-quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 1, timeout = 100, expect = counterexample]
+quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, timeout = 100, expect = counterexample]
 oops