src/HOL/Lattices.thy
2016-09-07 haftmann 2016-09-07 discontinued theory-local special syntax for lattice orderings
2016-08-10 haftmann 2016-08-10 formal passive interpretation proofs for conj and disj
2016-08-02 wenzelm 2016-08-02 misc tuning and modernization;
2016-06-20 wenzelm 2016-06-20 misc tuning and modernization;
2016-06-11 haftmann 2016-06-11 boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-11 Andreas Lochbihler 2015-11-11 cancel complementary terms as arguments to sup/inf in boolean algebras
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-02-15 haftmann 2015-02-15 explicit equivalence for strict order on lattices
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2013-12-25 haftmann 2013-12-25 explicit distributivity facts on min/max
2013-12-25 haftmann 2013-12-25 postponed min/max lemmas until abstract lattice is available
2013-12-25 haftmann 2013-12-25 prefer abstract simp rule
2013-12-25 haftmann 2013-12-25 more lemmas on abstract lattices
2013-12-24 haftmann 2013-12-24 tuning and augmentation of min/max lemmas; more lemmas and simp rules for abstract lattices with order; tuned proofs
2013-11-21 blanchet 2013-11-21 rationalize imports
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-05-26 haftmann 2013-05-26 examples for interpretation into target
2013-04-01 nipkow 2013-04-01 added lemma
2013-03-26 haftmann 2013-03-26 more uniform style for interpretation and sublocale declarations
2013-03-26 haftmann 2013-03-26 explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2013-03-23 haftmann 2013-03-23 locales for abstract orders
2013-03-10 nipkow 2013-03-10 stepwise instantiation is more modular
2012-12-22 nipkow 2012-12-22 added simp rule
2012-10-10 haftmann 2012-10-10 more explicit code equations
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