| #
9c73224b |
|
20-Jul-2018 |
Andreas Lochbihler <none@none> |
add lemmas about prod_filter
|
| #
2e1dc87f |
|
28-Mar-2018 |
huffman <none@none> |
tuned some proofs about filters
--HG--
extra : transplant_source : %E6L%A5l%05%CA%E6i%F3%FC%F4%D8%97%DE%BA%83%E8%9D%88%91
|
| #
2073516d |
|
26-Mar-2018 |
Manuel Eberl <eberlm@in.tum.de> |
Added some simple facts about limits
|
| #
b35f9468 |
|
14-Mar-2018 |
wenzelm <none@none> |
misc tuning and clarification;
|
| #
f408d13d |
|
23-Feb-2018 |
Wenda Li <wl302@cam.ac.uk> |
Unified the order of zeros and poles; improved reasoning around non-essential singularites
--HG--
extra : amend_source : 528e99138923389ffcb3b2021c959a3c9f20de52
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
7c894eca |
|
16-Feb-2018 |
Andreas Lochbihler <none@none> |
strengthen filter relator to canonical categorical definition with better properties
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
2ced7618 |
|
23-Jun-2017 |
eberlm <eberlm@in.tum.de> |
distrib_lattice instance for filters
|
| #
45af5ce6 |
|
22-Jun-2017 |
eberlm <eberlm@in.tum.de> |
Contravariant map on filters
|
| #
d244f158 |
|
25-Apr-2017 |
paulson <lp15@cam.ac.uk> |
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
|
| #
657eacc4 |
|
30-Sep-2016 |
paulson <lp15@cam.ac.uk> |
new material on paths, etc. Also rationalisation
|
| #
892044d3 |
|
28-Jul-2016 |
immler <none@none> |
numerical bounds on pi
|
| #
14001a0d |
|
22-Jul-2016 |
wenzelm <none@none> |
tuned proofs -- avoid unstructured calculation;
|
| #
48473ab7 |
|
22-Jun-2016 |
wenzelm <none@none> |
bundle lifting_syntax;
|
| #
259fcfd2 |
|
22-Feb-2016 |
paulson <lp15@cam.ac.uk> |
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
|
| #
3a51760b |
|
19-Feb-2016 |
hoelzl <none@none> |
generalize more theorems to support enat and ennreal
--HG--
extra : rebase_source : 11176604a37483aa41462153f0aa289df506590d
|
| #
c84c7ed2 |
|
08-Feb-2016 |
hoelzl <none@none> |
instantiate topologies for nat, int and enat
--HG--
extra : rebase_source : 2320da44d4913f441c671ef425945fac6d4381c9
|
| #
e826cd24 |
|
08-Feb-2016 |
hoelzl <none@none> |
move product topology to HOL-Complex_Main
--HG--
extra : rebase_source : 80e22139dd7e4e8ac20bba89047fdda51008fbef
|
| #
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
| #
1034afd6 |
|
11-Jan-2016 |
hoelzl <none@none> |
setup code generation for filters as suggested by Florian
|
| #
ec265e34 |
|
08-Jan-2016 |
hoelzl <none@none> |
fix code generation for uniformity: uniformity is a non-computable pure data.
|
| #
da01cc11 |
|
08-Jan-2016 |
hoelzl <none@none> |
add uniform spaces
|
| #
0bfb73b6 |
|
28-Dec-2015 |
wenzelm <none@none> |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
| #
3a79390c |
|
28-Dec-2015 |
wenzelm <none@none> |
use symbols by default;
|
| #
369e4785 |
|
13-Dec-2015 |
wenzelm <none@none> |
more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;
|
| #
474064bd |
|
09-Dec-2015 |
paulson <lp15@cam.ac.uk> |
sorted out eventually_mono
|
| #
c2655464 |
|
07-Dec-2015 |
paulson <lp15@cam.ac.uk> |
Cauchy's integral formula for circles. Starting to fix eventually_mono.
|
| #
dd88f1ec |
|
02-Nov-2015 |
eberlm <none@none> |
Rounding function, uniform limits, cotangent, binomial identities
|
| #
607ae3e3 |
|
09-Oct-2015 |
wenzelm <none@none> |
discontinued specific HTML syntax;
|
| #
f4007c81 |
|
25-Sep-2015 |
hoelzl <none@none> |
prove Liminf_inverse_ereal
--HG--
extra : rebase_source : 7d8a9342e5dbe92c85b912b98c1ce573397ea836
|
| #
848e0b58 |
|
22-Sep-2015 |
paulson <lp15@cam.ac.uk> |
Prepared two non-terminating proofs; no obvious link with my changes
|
| #
5eeb10d5 |
|
19-Aug-2015 |
paulson <lp15@cam.ac.uk> |
New material and fixes related to the forthcoming Stone-Weierstrass development
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
62ae9c62 |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
2156c498 |
|
14-Jul-2015 |
hoelzl <none@none> |
generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
|
| #
b1c0626f |
|
26-Jun-2015 |
wenzelm <none@none> |
do not expose goal parameters;
|
| #
c1b490ae |
|
07-May-2015 |
hoelzl <none@none> |
generalized tends over powr; added DERIV rule for powr
--HG--
extra : rebase_source : e5262f95063d694a1b08a65810ad2c515d8583a6
|
| #
22fd386c |
|
12-Apr-2015 |
hoelzl <none@none> |
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
|
| #
bead30ce |
|
12-Apr-2015 |
hoelzl <none@none> |
add cofinite filter
|
| #
d230579e |
|
12-Apr-2015 |
hoelzl <none@none> |
add frequently as dual for eventually
|
| #
ec5110b5 |
|
12-Apr-2015 |
hoelzl <none@none> |
add quantifier syntax for eventually
|
| #
8c7688c9 |
|
12-Apr-2015 |
hoelzl <none@none> |
move filters to their own theory
--HG--
rename : src/HOL/NSA/Filter.thy => src/HOL/NSA/Free_Ultrafilter.thy
|