src/HOL/Lattices.thy
2009-01-21 haftmann 2009-01-21 dropped ID
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
2008-12-11 ballarin 2008-12-11 Conversion of HOL-Main and ZF to new locales.
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-10-27 haftmann 2008-10-27 sup_bot and inf_top
2008-10-24 haftmann 2008-10-24 new classes "top" and "bot"
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-07-25 haftmann 2008-07-25 added class preorder
2008-05-07 berghofe 2008-05-07 - Now imports Fun rather than Orderings - Moved "Set as lattice" section behind "Fun as lattice" section, since sets are just functions. - The instantiations instantiation set :: (type) distrib_lattice instantiation set :: (type) complete_lattice are no longer needed, and the former definitions inf_set_eq, sup_set_eq, Inf_set_def, and Sup_set_def can now be derived from abstract properties of sup, inf, etc.
2008-03-07 haftmann 2008-03-07 tuned proofs
2008-01-30 haftmann 2008-01-30 dual orders and dual lattices
2007-11-30 haftmann 2007-11-30 adjustions to due to instance target
2007-11-28 haftmann 2007-11-28 dropped implicit assumption proof
2007-11-10 wenzelm 2007-11-10 tuned specifications of 'notation';
2007-10-26 haftmann 2007-10-26 localized monotonicity; tuned syntax
2007-10-19 haftmann 2007-10-19 antisymmetry not a default intro rule any longer
2007-10-16 haftmann 2007-10-16 global class syntax
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