src/HOL/Lattices.thy
2007-09-29 haftmann 2007-09-29 further localization
2007-09-18 ballarin 2007-09-18 Simplified proofs due to transitivity reasoner setup.
2007-09-01 wenzelm 2007-09-01 mono_Int/Un: proper proof, avoid illegal schematic type vars; removed obsolete ML bindings;
2007-08-20 haftmann 2007-08-20 Sup now explicit parameter of complete_lattice
2007-08-07 haftmann 2007-08-07 tuned
2007-07-24 haftmann 2007-07-24 using class target
2007-07-20 haftmann 2007-07-20 simplified HOL bootstrap
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-05-24 haftmann 2007-05-24 rudimentary class target implementation
2007-05-19 haftmann 2007-05-19 no special treatment in naming of locale predicates stemming form classes
2007-05-10 haftmann 2007-05-10 tuned
2007-04-20 haftmann 2007-04-20 tuned
2007-03-29 haftmann 2007-03-29 dropped legacy ML bindings
2007-03-16 haftmann 2007-03-16 integrated with LOrder.thy
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-03-02 haftmann 2007-03-02 prefix of class interpretation not mandatory any longer
2007-01-22 nipkow 2007-01-22 simplified proofs
2007-01-20 wenzelm 2007-01-20 tuned ML setup;
2007-01-16 haftmann 2007-01-16 renamed locale partial_order to order
2006-12-10 nipkow 2006-12-10 renaming
2006-12-10 nipkow 2006-12-10 Modified lattice locale
2006-12-01 haftmann 2006-12-01 stripped some legacy bindings
2006-11-15 haftmann 2006-11-15 reworking of min/max lemmas
2006-11-12 nipkow 2006-11-12 started reorgnization of lattice theories
2006-11-08 haftmann 2006-11-08 renamed Lattice_Locales to Lattices