changeset 42434 | 1914fd5d7c0e |
parent 42159 | 234ec7011e5d |
child 42696 | 7c7ca3fc7ce5 |
--- 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