Re: [isabelle] 3 new AFP entries

What's about formalizing in Isabelle the concept of dual lattices using locales? ( I haven’t found the word :"dual" in Lattice_Infix.)

I noted previously that to do this one need the ability to define locales inside locales, and Isabelle misses this.

Will this every be done?

27.09.2011, 12:26, "Gerwin Klein" <Gerwin.Klein at>:
 We are please to announce the availability of 3 new AFP entries at [].

 This brings the number of AFP entries over 100!

 1. Lattice Properties by Viorel Preoteasa

 This formalization introduces and collects some algebraic structures based on lattices and complete lattices for use in other developments. The structures introduced are complete distributive lattices, modular and distributive lattices, as well as lattice ordered groups. In addition to the results proved for the new lattices, this formalization also introduces theorems about latices and distributive lattices in general.
Victor Porton -

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.