Quickcheck_Types is no longer needed due to 51aa30c9ee4e
authorAndreas Lochbihler
Wed Aug 13 14:57:16 2014 +0200 (2014-08-13)
changeset 579219225b2761126
parent 57920 c1953856cfca
child 57922 dc78785427d0
Quickcheck_Types is no longer needed due to 51aa30c9ee4e
src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
     1.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy	Tue Aug 12 21:29:50 2014 +0200
     1.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy	Wed Aug 13 14:57:16 2014 +0200
     1.3 @@ -4,9 +4,11 @@
     1.4  *)
     1.5  
     1.6  theory Quickcheck_Lattice_Examples
     1.7 -imports "~~/src/HOL/Library/Quickcheck_Types"
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11 +declare [[quickcheck_finite_type_size=5]]
    1.12 +
    1.13  text {* We show how other default types help to find counterexamples to propositions if
    1.14    the standard default type @{typ int} is insufficient. *}
    1.15