| Mon, 12 Mar 2018 20:52:53 +0100 |
Manuel Eberl |
Changes to complete distributive lattices due to Viorel Preoteasa
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 16:44:45 +0000 |
paulson |
lots of new material, ultimately related to measure theory
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sun, 29 Jan 2017 17:27:02 +0100 |
wenzelm |
added inj_def (redundant, analogous to surj_def, bij_def);
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 14:14:49 +0100 |
paulson |
simple new lemmas, mostly about sets
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 11:59:09 +0200 |
haftmann |
discontinued theory-local special syntax for lattice orderings
|
file |
diff |
annotate
|
| Mon, 01 Aug 2016 22:36:47 +0200 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
| Mon, 01 Aug 2016 22:11:29 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2016 17:14:17 +0100 |
paulson |
lots of new theorems about differentiable_on, retracts, ANRs, etc.
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 08:41:05 +0200 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Fri, 27 May 2016 23:58:24 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 17 May 2016 17:05:35 +0200 |
eberlm |
Moved material from AFP/Randomised_Social_Choice to distribution
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 16:15:31 +0200 |
wenzelm |
explicit property for unbreakable block;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Sun, 03 Jan 2016 21:45:34 +0100 |
wenzelm |
retain ASCII syntax for output, when HOL/Library/Lattice_Syntax is not present (amending e96292f32c3c);
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 21:47:32 +0100 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 17:43:30 +0100 |
wenzelm |
prefer symbols for "Union", "Inter";
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 11 Nov 2015 09:48:24 +0100 |
Andreas Lochbihler |
add various lemmas
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 26 Jun 2015 10:20:33 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 28 May 2015 14:33:35 +0100 |
paulson |
Convex hulls: theorems about interior, etc. And a few simple lemmas.
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 15:45:25 +0200 |
hoelzl |
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
|
file |
diff |
annotate
|
| Mon, 09 Jun 2014 12:36:22 +0200 |
nipkow |
Sup/Inf on functions decoupled from complete_lattice.
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 13:25:46 +0200 |
haftmann |
subsumed by existing default simp rules for functions and booleans
|
file |
diff |
annotate
|