# HG changeset patch
# User bulwahn
# Date 1299853273 -3600
# Node ID a369f8ba5425f47a6058cf254b52fa9f4cdc84df
# Parent  9792a882da9c6aa7979d475c1afa349f71bbf2fc
adapting example file to renaming of the quickcheck tester

diff -r 9792a882da9c -r a369f8ba5425 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 11 15:21:13 2011 +0100
@@ -6,13 +6,13 @@
 header {* Examples for narrowing-based testing  *}
 
 theory Quickcheck_Narrowing_Examples
-imports "~~/src/HOL/Library/LSC"
+imports "~~/src/HOL/Library/Quickcheck_Narrowing"
 begin
 
 subsection {* Simple list examples *}
 
 lemma "rev xs = xs"
-quickcheck[tester = lazy_exhaustive, finite_types = false, default_type = nat, expect = counterexample]
+quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
 oops
 
 text {* Example fails due to some strange thing... *}
@@ -134,7 +134,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 = lazy_exhaustive, finite_types = false, default_type = nat, size = 1, timeout = 100, expect = counterexample]
+quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 1, timeout = 100, expect = counterexample]
 oops