# HG changeset patch
# User Andreas Lochbihler
# Date 1407934636 -7200
# Node ID 9225b2761126566fe6ebd8830bcaac66991e6aa3
# Parent  c1953856cfcaf2ea0c4f255714ce8b91aba127f6
Quickcheck_Types is no longer needed due to 51aa30c9ee4e

diff -r c1953856cfca -r 9225b2761126 src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
--- 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. *}