src/HOL/Complete_Lattices.thy
Sun, 29 Jan 2017 17:27:02 +0100 wenzelm added inj_def (redundant, analogous to surj_def, bij_def);
Thu, 15 Sep 2016 14:14:49 +0100 paulson simple new lemmas, mostly about sets
Wed, 07 Sep 2016 11:59:09 +0200 haftmann discontinued theory-local special syntax for lattice orderings
Mon, 01 Aug 2016 22:36:47 +0200 wenzelm tuned proof;
Mon, 01 Aug 2016 22:11:29 +0200 wenzelm misc tuning and modernization;
Wed, 13 Jul 2016 17:14:17 +0100 paulson lots of new theorems about differentiable_on, retracts, ANRs, etc.
Sat, 02 Jul 2016 08:41:05 +0200 haftmann more theorems
Fri, 27 May 2016 23:58:24 +0200 wenzelm tuned proofs;
Tue, 17 May 2016 17:05:35 +0200 eberlm Moved material from AFP/Randomised_Social_Choice to distribution
Fri, 01 Apr 2016 16:15:31 +0200 wenzelm explicit property for unbreakable block;
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Sun, 03 Jan 2016 21:45:34 +0100 wenzelm retain ASCII syntax for output, when HOL/Library/Lattice_Syntax is not present (amending e96292f32c3c);
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Mon, 28 Dec 2015 17:43:30 +0100 wenzelm prefer symbols for "Union", "Inter";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 11 Nov 2015 09:48:24 +0100 Andreas Lochbihler add various lemmas
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Fri, 26 Jun 2015 10:20:33 +0200 wenzelm tuned whitespace;
Thu, 28 May 2015 14:33:35 +0100 paulson Convex hulls: theorems about interior, etc. And a few simple lemmas.
Mon, 04 May 2015 17:35:31 +0200 hoelzl rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Mon, 30 Jun 2014 15:45:25 +0200 hoelzl more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
Mon, 09 Jun 2014 12:36:22 +0200 nipkow Sup/Inf on functions decoupled from complete_lattice.
Sat, 26 Apr 2014 14:53:22 +0200 haftmann more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
Sat, 26 Apr 2014 13:25:46 +0200 haftmann subsumed by existing default simp rules for functions and booleans
Sat, 22 Mar 2014 08:37:43 +0100 haftmann generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
Wed, 19 Mar 2014 18:47:22 +0100 haftmann elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
Tue, 18 Mar 2014 22:11:46 +0100 haftmann consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Thu, 13 Mar 2014 08:56:08 +0100 haftmann dropped redundant theorems
Thu, 13 Mar 2014 08:56:07 +0100 haftmann monotonicity in complete lattices
Sun, 09 Mar 2014 22:45:09 +0100 haftmann bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices
Tue, 12 Nov 2013 19:28:54 +0100 hoelzl add equalities for SUP and INF over constant functions
Tue, 05 Nov 2013 09:44:59 +0100 hoelzl add SUP and INF for conditionally complete lattices
Tue, 05 Nov 2013 09:44:57 +0100 hoelzl generalize SUP and INF to the syntactic type classes Sup and Inf
Fri, 18 Oct 2013 10:43:20 +0200 blanchet killed most "no_atp", to make Sledgehammer more complete
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Thu, 25 Jul 2013 08:57:16 +0200 haftmann factored syntactic type classes for bot and top (by Alessandro Coglio)
Sat, 25 May 2013 15:44:29 +0200 haftmann weaker precendence of syntax for big intersection and union on sets
Tue, 26 Mar 2013 20:49:57 +0100 haftmann explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
Sat, 23 Mar 2013 20:50:39 +0100 haftmann fundamental revision of big operators on sets
Sun, 10 Mar 2013 11:21:16 +0100 haftmann generalized subclass relation;
Tue, 05 Mar 2013 15:43:12 +0100 hoelzl complete_linorder is also a complete_distrib_lattice
Wed, 20 Feb 2013 12:04:42 +0100 hoelzl move auxiliary lemmas from Library/Extended_Reals to HOL image
Thu, 18 Oct 2012 09:19:37 +0200 haftmann simp results for simplification results of Inf/Sup expressions on bool;
Mon, 12 Mar 2012 21:41:11 +0100 noschinl tuned proofs
Mon, 12 Mar 2012 15:11:24 +0100 noschinl tuned simpset
Sun, 26 Feb 2012 21:25:54 +0100 haftmann retain syntax here
Sun, 26 Feb 2012 20:10:14 +0100 haftmann tuned syntax declarations; tuned structure
Sun, 26 Feb 2012 15:28:48 +0100 haftmann marked candidates for rule declarations
Thu, 23 Feb 2012 20:33:35 +0100 haftmann moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
Tue, 21 Feb 2012 08:15:42 +0100 haftmann reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
Sun, 19 Feb 2012 15:30:35 +0100 haftmann distributed lattice properties of predicates to places of instantiation
Sat, 07 Jan 2012 20:18:56 +0100 haftmann use Inf/Sup_bool_def/apply as code equations
Thu, 29 Dec 2011 14:23:40 +0100 haftmann fundamental theorems on Set.bind
Sat, 24 Dec 2011 15:53:07 +0100 haftmann lattice type class instances for `set`; added code lemma for Set.bind
Tue, 20 Sep 2011 22:11:22 +0200 haftmann official status for UN_singleton
Mon, 19 Sep 2011 14:35:51 +0200 noschinl removed legacy lemmas in Complete_Lattices
less more (0) -60 tip