#
4ea7c69c |
|
04-Dec-2019 |
haftmann <none@none> |
removed some vain declarations --HG-- extra : rebase_source : 98c20947b793ce6b5ba40e21a5c180215fb77ab5
|
#
a042053d |
|
27-Oct-2019 |
nipkow <none@none> |
renamed because of duplicateion to avoid very long qualified names
|
#
21e3fdd1 |
|
14-Jun-2019 |
haftmann <none@none> |
removed relics of ASCII syntax for indexed big operators
|
#
945c5111 |
|
26-Mar-2019 |
paulson <lp15@cam.ac.uk> |
generalised homotopic_with to topologies; homotopic_with_canon is the old version
|
#
551b6192 |
|
05-Mar-2019 |
haftmann <none@none> |
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
|
#
e977f1fa |
|
31-Jan-2019 |
haftmann <none@none> |
proper congruence rule for image operator --HG-- extra : rebase_source : 71f59936260619419f4d3f7f86d1b930bc771065
|
#
e5238d11 |
|
28-Jan-2019 |
nipkow <none@none> |
more canonical and less specialized syntax
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
ec600d16 |
|
30-Dec-2018 |
haftmann <none@none> |
prefer naming convention from datatype package for strong congruence rules
|
#
ec8d5b30 |
|
10-Nov-2018 |
haftmann <none@none> |
clarified status of legacy input abbreviations
|
#
abcb385f |
|
10-Nov-2018 |
haftmann <none@none> |
clarified status of ancient ASCII syntax for big union and inter
|
#
97b2ecf5 |
|
08-Nov-2018 |
haftmann <none@none> |
removed relics of ASCII syntax for indexed big operators
|
#
6fd6219b |
|
21-Oct-2018 |
nipkow <none@none> |
uniform naming of strong congruence rules
|
#
11e8aae1 |
|
20-Sep-2018 |
paulson <lp15@cam.ac.uk> |
elimination of near duplication involving Rolle's theorem and the MVT
|
#
888b6a7c |
|
12-Sep-2018 |
nipkow <none@none> |
added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
|
#
6243d81c |
|
30-Aug-2018 |
Manuel Eberl <eberlm@in.tum.de> |
Some basic materials on filters and topology --HG-- extra : rebase_source : af17e025be84916013ccf7c6ca0f669ec047aa54
|
#
66f2eeda |
|
24-Aug-2018 |
haftmann <none@none> |
some modernization of notation --HG-- extra : rebase_source : 5e9836a69d8e9ea3e5e173b956099f5a132a6d8b
|
#
816751f9 |
|
24-Aug-2018 |
haftmann <none@none> |
deprecation of ASCII syntax for indexed big operators --HG-- extra : rebase_source : e97da5e40928653f480490ee2f24e33a701892a9
|
#
f46d113c |
|
23-Aug-2018 |
haftmann <none@none> |
tuned
|
#
50e7921e |
|
23-Aug-2018 |
haftmann <none@none> |
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
|
#
d5cfd618 |
|
23-Aug-2018 |
haftmann <none@none> |
dropped redundant syntax translation rules for big operators
|
#
965df47d |
|
12-Mar-2018 |
Manuel Eberl <eberlm@in.tum.de> |
Changes to complete distributive lattices due to Viorel Preoteasa
|
#
d463f754 |
|
19-Feb-2018 |
paulson <lp15@cam.ac.uk> |
lots of new material, ultimately related to measure theory
|
#
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
229f8947 |
|
29-Jan-2017 |
wenzelm <none@none> |
added inj_def (redundant, analogous to surj_def, bij_def); tuned proofs;
|
#
1e83a38a |
|
15-Sep-2016 |
paulson <lp15@cam.ac.uk> |
simple new lemmas, mostly about sets
|
#
58b13a3d |
|
07-Sep-2016 |
haftmann <none@none> |
discontinued theory-local special syntax for lattice orderings --HG-- extra : rebase_source : a43595e983fb7b5e8e9031a09ddee560d27e761b
|
#
cc60eb70 |
|
01-Aug-2016 |
wenzelm <none@none> |
tuned proof;
|
#
8806de60 |
|
01-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
6a621c7e |
|
13-Jul-2016 |
paulson <lp15@cam.ac.uk> |
lots of new theorems about differentiable_on, retracts, ANRs, etc.
|
#
0f0a91d1 |
|
02-Jul-2016 |
haftmann <none@none> |
more theorems
|
#
fb0c4f7e |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs;
|
#
94ba250a |
|
17-May-2016 |
eberlm <none@none> |
Moved material from AFP/Randomised_Social_Choice to distribution
|
#
772cb5d0 |
|
01-Apr-2016 |
wenzelm <none@none> |
explicit property for unbreakable block;
|
#
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
#
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
#
35275d1f |
|
03-Jan-2016 |
wenzelm <none@none> |
retain ASCII syntax for output, when HOL/Library/Lattice_Syntax is not present (amending e96292f32c3c);
|
#
0bfb73b6 |
|
28-Dec-2015 |
wenzelm <none@none> |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
#
6fc0f068 |
|
28-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "Union", "Inter";
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
3487f527 |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
add various lemmas
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
6f0c89b5 |
|
26-Jun-2015 |
wenzelm <none@none> |
tuned whitespace;
|
#
7f5fa27d |
|
28-May-2015 |
paulson <lp15@cam.ac.uk> |
Convex hulls: theorems about interior, etc. And a few simple lemmas.
|
#
66005bbd |
|
04-May-2015 |
hoelzl <none@none> |
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity --HG-- extra : rebase_source : 6c7faec3b6fc45b9da856e08add46f99a0b483b7
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
d37dfba9 |
|
30-Jun-2014 |
hoelzl <none@none> |
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs --HG-- extra : rebase_source : 8664c1d86ed72607199cc8197a480070514ae330
|
#
e10b892a |
|
08-Jun-2014 |
nipkow <none@none> |
Sup/Inf on functions decoupled from complete_lattice.
|
#
e121e77d |
|
26-Apr-2014 |
haftmann <none@none> |
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP) --HG-- extra : rebase_source : 710314bbc990dc6cb912a800546a75f7c3a07dca
|
#
914ea354 |
|
26-Apr-2014 |
haftmann <none@none> |
subsumed by existing default simp rules for functions and booleans --HG-- extra : rebase_source : ef9788dcfe4feeb0d38628d1d5a9fe004fb0b659
|
#
03184bca |
|
22-Mar-2014 |
haftmann <none@none> |
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
|
#
12157cd1 |
|
19-Mar-2014 |
haftmann <none@none> |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
#
15c7dcff |
|
18-Mar-2014 |
haftmann <none@none> |
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
|
#
4f5ebd94 |
|
16-Mar-2014 |
haftmann <none@none> |
normalising simp rules for compound operators
|
#
4ce02222 |
|
13-Mar-2014 |
haftmann <none@none> |
dropped redundant theorems
|
#
d7de4a1d |
|
13-Mar-2014 |
haftmann <none@none> |
monotonicity in complete lattices
|
#
42fc4ea5 |
|
09-Mar-2014 |
haftmann <none@none> |
bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices * * * tuned
|
#
8a6243a2 |
|
12-Nov-2013 |
hoelzl <none@none> |
add equalities for SUP and INF over constant functions
|
#
fd02713b |
|
05-Nov-2013 |
hoelzl <none@none> |
add SUP and INF for conditionally complete lattices
|
#
d8c6c2fb |
|
05-Nov-2013 |
hoelzl <none@none> |
generalize SUP and INF to the syntactic type classes Sup and Inf
|
#
03633065 |
|
18-Oct-2013 |
blanchet <none@none> |
killed most "no_atp", to make Sledgehammer more complete
|
#
7237bdd9 |
|
02-Sep-2013 |
wenzelm <none@none> |
tuned proofs -- clarified flow of facts wrt. calculation;
|
#
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
#
1612e9ff |
|
25-Jul-2013 |
haftmann <none@none> |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
#
ffb245a6 |
|
25-May-2013 |
haftmann <none@none> |
weaker precendence of syntax for big intersection and union on sets
|
#
de37771f |
|
26-Mar-2013 |
haftmann <none@none> |
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
|
#
d4cae3bf |
|
23-Mar-2013 |
haftmann <none@none> |
fundamental revision of big operators on sets
|
#
744f4078 |
|
10-Mar-2013 |
haftmann <none@none> |
generalized subclass relation; tuned proof
|
#
27a2df09 |
|
05-Mar-2013 |
hoelzl <none@none> |
complete_linorder is also a complete_distrib_lattice
|
#
cc794fdb |
|
19-Feb-2013 |
hoelzl <none@none> |
move auxiliary lemmas from Library/Extended_Reals to HOL image
|
#
c1d9f321 |
|
18-Oct-2012 |
haftmann <none@none> |
simp results for simplification results of Inf/Sup expressions on bool; tuned proofs
|
#
81c2aa38 |
|
12-Mar-2012 |
noschinl <none@none> |
tuned proofs
|
#
f9af5d85 |
|
12-Mar-2012 |
noschinl <none@none> |
tuned simpset
|
#
d12eea8e |
|
26-Feb-2012 |
haftmann <none@none> |
retain syntax here --HG-- extra : rebase_source : e0404cbbb00948257c361a89d62100a9adf74571
|
#
92c9b3bf |
|
26-Feb-2012 |
haftmann <none@none> |
tuned syntax declarations; tuned structure --HG-- extra : rebase_source : 1b6c21e91abe00bbf0ca93b6c0f5a24da0bef488
|
#
1cc410e1 |
|
26-Feb-2012 |
haftmann <none@none> |
marked candidates for rule declarations
|
#
f0c3a8ae |
|
23-Feb-2012 |
haftmann <none@none> |
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
|
#
98c01e6d |
|
21-Feb-2012 |
haftmann <none@none> |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
#
a8fde5da |
|
19-Feb-2012 |
haftmann <none@none> |
distributed lattice properties of predicates to places of instantiation --HG-- extra : rebase_source : f060e45b06e82cc14c73eba231a21e4636bbe179
|
#
d489f2fc |
|
07-Jan-2012 |
haftmann <none@none> |
use Inf/Sup_bool_def/apply as code equations --HG-- extra : rebase_source : 9822efe22960d359544f837617d3e6e106e3d18a
|
#
0c69faee |
|
29-Dec-2011 |
haftmann <none@none> |
fundamental theorems on Set.bind --HG-- extra : rebase_source : f60f78a12efe9f4496619a04d48afb38f7eccb9d
|
#
b5ed4da7 |
|
24-Dec-2011 |
haftmann <none@none> |
lattice type class instances for `set`; added code lemma for Set.bind
|
#
9b6e7a835 |
|
20-Sep-2011 |
haftmann <none@none> |
official status for UN_singleton
|
#
1732ff37 |
|
19-Sep-2011 |
noschinl <none@none> |
removed legacy lemmas in Complete_Lattices
|
#
ce0ab485 |
|
14-Sep-2011 |
hoelzl <none@none> |
removed further legacy rules from Complete_Lattices
|
#
15635718 |
|
13-Sep-2011 |
huffman <none@none> |
tuned proofs
|
#
ed821c16 |
|
13-Sep-2011 |
huffman <none@none> |
remove some redundant [simp] declarations; simplify some proofs;
|
#
551d75e2 |
|
13-Sep-2011 |
noschinl <none@none> |
tune proofs
|
#
a3372eca |
|
13-Sep-2011 |
noschinl <none@none> |
tune simpset for Complete_Lattices
|
#
7e65ae14 |
|
14-Sep-2011 |
hoelzl <none@none> |
renamed Complete_Lattices lemmas, removed legacy names
|
#
d04d4aee |
|
10-Sep-2011 |
haftmann <none@none> |
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc. --HG-- rename : src/HOL/Complete_Lattice.thy => src/HOL/Complete_Lattices.thy
|