--- a/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy Tue Aug 12 21:29:50 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy Wed Aug 13 14:57:16 2014 +0200
@@ -4,9 +4,11 @@
*)
theory Quickcheck_Lattice_Examples
-imports "~~/src/HOL/Library/Quickcheck_Types"
+imports Main
begin
+declare [[quickcheck_finite_type_size=5]]
+
text {* We show how other default types help to find counterexamples to propositions if
the standard default type @{typ int} is insufficient. *}