Re: [isabelle] 3 new AFP entries

Hello Victor,

The class lattice_infix is just a wrapper around the lattice class from
the standard Isabelle library. I added this class just as a work around
for some feature that I could not get directly from the library.

However lattice_infix will become obsolete with the next release of
Isabelle which adds support for the features built in lattice_infix.

Best regards,


On 9/27/11 8:01 AM, Victor Porton wrote:
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.

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