src/HOL/Library/Product_Lattice.thy
changeset 50573 765c22baa1c9
parent 50535 2464d77527c4
equal deleted inserted replaced
50572:b33912e68b84 50573:765c22baa1c9
   220 by (metis fst_SUP snd_SUP surjective_pairing)
   220 by (metis fst_SUP snd_SUP surjective_pairing)
   221 
   221 
   222 
   222 
   223 subsection {* Complete distributive lattices *}
   223 subsection {* Complete distributive lattices *}
   224 
   224 
   225 (* Contribution: Allesandro Coglio *)
   225 (* Contribution: Alessandro Coglio *)
   226 
   226 
   227 instance prod ::
   227 instance prod ::
   228   (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
   228   (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
   229 proof
   229 proof
   230   case goal1 thus ?case
   230   case goal1 thus ?case