src/HOL/Lattices.thy
2012-03-12 noschinl 2012-03-12 tuned proofs
2012-03-12 noschinl 2012-03-12 tuned simpset
2012-02-26 haftmann 2012-02-26 tuned syntax declarations; tuned structure
2012-02-26 haftmann 2012-02-26 marked candidates for rule declarations
2012-02-23 haftmann 2012-02-23 moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
2012-02-21 haftmann 2012-02-21 reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
2012-02-19 haftmann 2012-02-19 distributed lattice properties of predicates to places of instantiation
2011-09-13 huffman 2011-09-13 tuned proofs
2011-09-13 noschinl 2011-09-13 tune proofs
2011-09-13 noschinl 2011-09-13 tune simpset for Complete_Lattices
2011-09-09 krauss 2011-09-09 added syntactic classes for "inf" and "sup"
2011-08-08 haftmann 2011-08-08 move legacy candiates to bottom; marked candidates for default simp rules
2011-07-17 haftmann 2011-07-17 more on complement
2011-07-10 haftmann 2011-07-10 tuned notation
2010-12-08 haftmann 2010-12-08 bot comes before top, inf before sup etc.
2010-12-08 haftmann 2010-12-08 nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules
2010-12-08 haftmann 2010-12-08 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
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