# 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