src/HOL/Algebra/Lattice.thy
21 months ago wenzelm 2018-01-16 standardized towards new-style formal comments: isabelle update_comments;
22 months ago wenzelm 2017-12-19 isabelle update_cartouches -c -t;
23 months ago wenzelm 2017-11-26 more symbols;
2017-08-31 ballarin 2017-08-31 Avoid \mu and \nu as constant syntax, use LFP and GFP instead.
2017-03-02 ballarin 2017-03-02 Knaster-Tarski fixed point theorem and Galois Connections.
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2015-11-04 ballarin 2015-11-04 Qualifiers in locale expressions default to mandatory regardless of the command.
2015-10-10 wenzelm 2015-10-10 isabelle update_cartouches;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-06-26 wenzelm 2015-06-26 tuned whitespace;
2014-03-05 wenzelm 2014-03-05 more symbols;
2011-12-28 wenzelm 2011-12-28 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008"; tuned proofs;
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-02 wenzelm 2011-09-02 tuned proofs;
2011-08-24 wenzelm 2011-08-24 tuned proofs;
2010-10-31 ballarin 2010-10-31 Minor reformat.
2010-10-12 krauss 2010-10-12 slightly more robust proof
2010-03-21 wenzelm 2010-03-21 standard headers;
2010-03-21 wenzelm 2010-03-21 slightly more uniform definitions -- eliminated old-style meta-equality;
2010-03-21 wenzelm 2010-03-21 eliminated old constdefs;
2009-11-13 nipkow 2009-11-13 renamed lemmas "anti_sym" -> "antisym"
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-03-08 wenzelm 2009-03-08 proper local context for text with antiquotations;
2008-12-19 ballarin 2008-12-19 More porting to new locales
2008-12-16 ballarin 2008-12-16 More porting to new locales.
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-08-01 ballarin 2008-08-01 Generalised polynomial lemmas from cring to ring.
2008-07-31 ballarin 2008-07-31 Tuned (for the sake of a meaningless log entry).
2008-07-30 ballarin 2008-07-30 New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-29 ballarin 2008-07-29 Renamed theorems; New theory on divisibility.
2008-05-07 berghofe 2008-05-07 Replaced forward proofs of existential statements by backward proofs to avoid problems with HO unification
2007-07-31 ballarin 2007-07-31 Proper interpretation of total orders in lattices.
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-02-07 berghofe 2007-02-07 Adapted to changes in Finite_Set theory.
2007-01-12 ballarin 2007-01-12 Reverted to structure representation with records.
2006-12-22 ballarin 2006-12-22 Experimenting with interpretations of "definition".
2006-12-05 wenzelm 2006-12-05 removed duplicate abbreviations (implicit inheritance);
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-10-18 ballarin 2006-10-18 Stylistic improvements.
2006-10-16 ballarin 2006-10-16 Order and lattice structures no longer based on records.
2006-08-03 ballarin 2006-08-03 Restructured algebra library, added ideals and quotient rings.
2006-07-04 ballarin 2006-07-04 Method intro_locales replaced by intro_locales and unfold_locales.
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2006-06-06 ballarin 2006-06-06 Improved parameter management of locales.
2006-03-18 haftmann 2006-03-18 renamed constant less in lattice
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-06-08 ballarin 2005-06-08 Fixed "axiom" generation for mixed locales with and without predicates.
2004-11-24 nipkow 2004-11-24 mod because of change in finite set induction
2004-05-14 ballarin 2004-05-14 Change of theory hierarchy: Group is now based in Lattice.
2004-05-06 wenzelm 2004-05-06 tuned document;
2004-05-01 wenzelm 2004-05-01 improved syntax;
2004-04-23 wenzelm 2004-04-23 improved notation;
2004-04-22 wenzelm 2004-04-22 improved notation;
2004-04-16 wenzelm 2004-04-16 tuned document;
2004-04-13 ballarin 2004-04-13 Various changes to HOL-Algebra; Locale instantiation.