# 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: "\ is_ord(MKT (x :: nat) l r h); height l = height r + 2 \ \ 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