author | bulwahn |
Wed, 20 Apr 2011 16:00:45 +0200 | |
changeset 42434 | 1914fd5d7c0e |
parent 42433 | b48d9186e883 |
child 42435 | c3d880b13aa9 |
--- a/src/HOL/ex/Quickcheck_Examples.thy Wed Apr 20 16:00:44 2011 +0200 +++ b/src/HOL/ex/Quickcheck_Examples.thy Wed Apr 20 16:00:45 2011 +0200 @@ -294,4 +294,28 @@ quickcheck[random, size = 10] oops +subsection {* Examples with locales *} + +locale Truth + +context Truth +begin + +lemma "False" +quickcheck[expect = no_counterexample] +oops + end + +interpretation Truth . + +context Truth +begin + +lemma "False" +quickcheck[expect = counterexample] +oops + +end + +end