src/HOL/ex/Quickcheck_Lattice_Examples.thy
changeset 43888 ee4be704c2a4
parent 41413 64cd30d6b0b8
child 44845 5e51075cbd97
     1.1 --- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Mon Jul 18 10:34:21 2011 +0200
     1.2 +++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Mon Jul 18 10:34:21 2011 +0200
     1.3 @@ -18,6 +18,8 @@
     1.4    inf (infixl "\<sqinter>" 70) and
     1.5    sup (infixl "\<squnion>" 65)
     1.6  
     1.7 +declare [[quickcheck_narrowing_active = false]]
     1.8 +
     1.9  subsection {* Distributive lattices *}
    1.10  
    1.11  lemma sup_inf_distrib2: