src/HOL/Complete_Lattices.thy
2017-01-29 wenzelm 2017-01-29 added inj_def (redundant, analogous to surj_def, bij_def); tuned proofs;
2016-09-15 paulson 2016-09-15 simple new lemmas, mostly about sets
2016-09-07 haftmann 2016-09-07 discontinued theory-local special syntax for lattice orderings
2016-08-01 wenzelm 2016-08-01 tuned proof;
2016-08-01 wenzelm 2016-08-01 misc tuning and modernization;
2016-07-13 paulson 2016-07-13 lots of new theorems about differentiable_on, retracts, ANRs, etc.
2016-07-02 haftmann 2016-07-02 more theorems
2016-05-27 wenzelm 2016-05-27 tuned proofs;
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-04-01 wenzelm 2016-04-01 explicit property for unbreakable block;
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-01-03 wenzelm 2016-01-03 retain ASCII syntax for output, when HOL/Library/Lattice_Syntax is not present (amending e96292f32c3c);
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-28 wenzelm 2015-12-28 prefer symbols for "Union", "Inter";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-26 wenzelm 2015-06-26 tuned whitespace;
2015-05-28 paulson 2015-05-28 Convex hulls: theorems about interior, etc. And a few simple lemmas.
2015-05-04 hoelzl 2015-05-04 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-06-30 hoelzl 2014-06-30 more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
2014-06-09 nipkow 2014-06-09 Sup/Inf on functions decoupled from complete_lattice.
2014-04-26 haftmann 2014-04-26 more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
2014-04-26 haftmann 2014-04-26 subsumed by existing default simp rules for functions and booleans
2014-03-22 haftmann 2014-03-22 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-13 haftmann 2014-03-13 dropped redundant theorems
2014-03-13 haftmann 2014-03-13 monotonicity in complete lattices
2014-03-09 haftmann 2014-03-09 bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices * * * tuned
2013-11-12 hoelzl 2013-11-12 add equalities for SUP and INF over constant functions
2013-11-05 hoelzl 2013-11-05 add SUP and INF for conditionally complete lattices
2013-11-05 hoelzl 2013-11-05 generalize SUP and INF to the syntactic type classes Sup and Inf
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-05-25 haftmann 2013-05-25 weaker precendence of syntax for big intersection and union on sets
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-10 haftmann 2013-03-10 generalized subclass relation; tuned proof
2013-03-05 hoelzl 2013-03-05 complete_linorder is also a complete_distrib_lattice
2013-02-20 hoelzl 2013-02-20 move auxiliary lemmas from Library/Extended_Reals to HOL image
2012-10-18 haftmann 2012-10-18 simp results for simplification results of Inf/Sup expressions on bool; tuned proofs
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 retain syntax here
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
2012-01-07 haftmann 2012-01-07 use Inf/Sup_bool_def/apply as code equations
2011-12-29 haftmann 2011-12-29 fundamental theorems on Set.bind
2011-12-24 haftmann 2011-12-24 lattice type class instances for `set`; added code lemma for Set.bind
2011-09-20 haftmann 2011-09-20 official status for UN_singleton
2011-09-19 noschinl 2011-09-19 removed legacy lemmas in Complete_Lattices