src/HOL/ex/Quickcheck_Lattice_Examples.thy
changeset 44845 5e51075cbd97
parent 43888 ee4be704c2a4
child 44994 a915907a67d5
     1.1 --- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Thu Sep 08 08:41:28 2011 -0700
     1.2 +++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Fri Sep 09 00:22:18 2011 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4    by (rule inf_absorb1) simp
     1.5  
     1.6  lemma inf_eq_top_iff [simp]:
     1.7 -  "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
     1.8 +  "(x :: 'a :: bounded_lattice_top) \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
     1.9    quickcheck[expect = no_counterexample]
    1.10    by (simp add: eq_iff)
    1.11