diff -r 2da02764d523 -r 52551c0a3374 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 @@ -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