src/HOL/Complete_Lattices.thy
Tue, 26 Mar 2019 17:01:36 +0000 paulson generalised homotopic_with to topologies; homotopic_with_canon is the old version
Tue, 05 Mar 2019 07:00:21 +0000 haftmann avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
Thu, 31 Jan 2019 13:08:59 +0000 haftmann proper congruence rule for image operator
Mon, 28 Jan 2019 10:27:47 +0100 nipkow more canonical and less specialized syntax
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sun, 30 Dec 2018 10:34:56 +0000 haftmann prefer naming convention from datatype package for strong congruence rules
Sat, 10 Nov 2018 07:57:19 +0000 haftmann clarified status of legacy input abbreviations
Sat, 10 Nov 2018 07:57:18 +0000 haftmann clarified status of ancient ASCII syntax for big union and inter
Thu, 08 Nov 2018 09:11:52 +0100 haftmann removed relics of ASCII syntax for indexed big operators
Sun, 21 Oct 2018 09:39:09 +0200 nipkow uniform naming of strong congruence rules
Thu, 20 Sep 2018 14:17:58 +0100 paulson elimination of near duplication involving Rolle's theorem and the MVT
Wed, 12 Sep 2018 18:44:31 +0200 nipkow added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
Thu, 30 Aug 2018 17:20:54 +0200 Manuel Eberl Some basic materials on filters and topology
Fri, 24 Aug 2018 20:22:14 +0000 haftmann some modernization of notation
Fri, 24 Aug 2018 20:22:10 +0000 haftmann deprecation of ASCII syntax for indexed big operators
Thu, 23 Aug 2018 17:10:28 +0000 haftmann tuned
Thu, 23 Aug 2018 17:09:39 +0000 haftmann simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
Thu, 23 Aug 2018 17:09:37 +0000 haftmann dropped redundant syntax translation rules for big operators
Mon, 12 Mar 2018 20:52:53 +0100 Manuel Eberl Changes to complete distributive lattices due to Viorel Preoteasa
Mon, 19 Feb 2018 16:44:45 +0000 paulson lots of new material, ultimately related to measure theory
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
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;
less more (0) -60 tip