src/HOL/Lattices.thy
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-05-05 haftmann 2010-05-05 tuned whitespace
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-04-26 Cezary Kaliszyk 2010-04-26 add bounded_lattice_bot and bounded_lattice_top type classes
2010-04-07 ballarin 2010-04-07 Merged resolving conflicts NEWS and locale.ML.
2010-02-15 ballarin 2010-02-15 Tuned interpretation proofs.
2010-03-28 huffman 2010-03-28 add/change some lemmas about lattices
2010-03-11 haftmann 2010-03-11 fixed typo
2010-02-22 haftmann 2010-02-22 distributed theory Algebras to theories Groups and Lattices
2010-02-12 haftmann 2010-02-12 tuned import order
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-28 haftmann 2010-01-28 dropped mk_left_commute; use interpretation of locale abel_semigroup instead
2009-12-30 krauss 2009-12-30 killed a few warnings
2009-12-05 haftmann 2009-12-05 tuned lattices theory fragements; generlized some lemmas from sets to lattices
2009-09-30 haftmann 2009-09-30 moved lemmas about sup on bool to Lattices.thy
2009-09-30 haftmann 2009-09-30 tuned proofs
2009-09-22 haftmann 2009-09-22 be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
2009-09-14 haftmann 2009-09-14 some lemmas about strict order in lattices
2009-09-03 haftmann 2009-09-03 proper class syntax for sublocale class < expr
2009-08-28 nipkow 2009-08-28 Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
2009-07-25 haftmann 2009-07-25 localized interpretation of min/max-lattice
2009-07-14 haftmann 2009-07-14 refinement of lattice classes
2009-07-13 haftmann 2009-07-13 removed outdated comment
2009-07-11 haftmann 2009-07-11 added boolean_algebra type class; tuned lattice duals
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-05 haftmann 2009-03-05 moved complete_lattice to Set.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