# HG changeset patch # User bulwahn # Date 1303308045 -7200 # Node ID 1914fd5d7c0ea0986c0e9fbb3cc148a0126e7951 # Parent b48d9186e883e1782c460156aaae2d37b07ead52 adding examples for Quickcheck used within locales diff -r b48d9186e883 -r 1914fd5d7c0e src/HOL/ex/Quickcheck_Examples.thy --- 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