#
1a8dfc75 |
|
14-Mar-2020 |
paulson <lp15@cam.ac.uk> |
tidied up a few little proofs
|
#
a4784f6f |
|
09-Oct-2019 |
haftmann <none@none> |
dedicated fact collections for algebraic simplification rules potentially splitting goals --HG-- extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6
|
#
5fccd0bf |
|
08-Oct-2019 |
haftmann <none@none> |
formally augmented corresponding rules for field_simps --HG-- extra : rebase_source : 10a72e1ed5967c95cb98493db93fec6c7d0f8230
|
#
a1f8bb2d |
|
18-Sep-2019 |
paulson <lp15@cam.ac.uk> |
imported new material mostly due to Sébastien Gouëzel
|
#
5f3b0e28 |
|
28-Aug-2019 |
haftmann <none@none> |
more rules for ordered real vector spaces
|
#
d722beb6 |
|
27-Aug-2019 |
immler <none@none> |
explicit instance real::ordered_real_vector before subclass in ordered_euclidean_space
|
#
075e0a05 |
|
01-Apr-2019 |
paulson <lp15@cam.ac.uk> |
A few results in Algebra, and bits for Analysis
|
#
083015db |
|
21-Jan-2019 |
paulson <lp15@cam.ac.uk> |
new material about summations and powers, along with some tweaks
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
15438984 |
|
27-Dec-2018 |
immler <none@none> |
moved lemmas up
|
#
1a4d151d |
|
27-Dec-2018 |
immler <none@none> |
prove lemmas in context real_normed_vector
|
#
97b2ecf5 |
|
08-Nov-2018 |
haftmann <none@none> |
removed relics of ASCII syntax for indexed big operators
|
#
cc37beb1 |
|
24-Sep-2018 |
nipkow <none@none> |
Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
|
#
0fdd6bca |
|
03-Aug-2018 |
eberlm <eberlm@in.tum.de> |
Small lemmas about analysis --HG-- extra : rebase_source : d857a4b442d3d409faf82354bcbb2e39b5445956
|
#
830577aa |
|
21-Jul-2018 |
paulson <lp15@cam.ac.uk> |
de-applying and removing junk
|
#
0277d8a8 |
|
11-Jul-2018 |
paulson <lp15@cam.ac.uk> |
de-applying
|
#
3f439188 |
|
05-Jul-2018 |
paulson <lp15@cam.ac.uk> |
de-applying
|
#
1394cb87 |
|
28-Jun-2018 |
paulson <lp15@cam.ac.uk> |
Incorporating new/strengthened proofs from Library and AFP entries
|
#
102fb118 |
|
26-Jun-2018 |
paulson <lp15@cam.ac.uk> |
Rationalisation of complex transcendentals, esp the Arg function
|
#
7bd366c3 |
|
18-Jun-2018 |
paulson <lp15@cam.ac.uk> |
New material in support of quaternions
|
#
dcc6865b |
|
06-Jun-2018 |
wenzelm <none@none> |
isabelle update_comments;
|
#
e04b7748 |
|
02-May-2018 |
immler <none@none> |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly --HG-- rename : src/HOL/Library/FuncSet.thy => src/HOL/FuncSet.thy
|
#
78eb1fe1 |
|
25-Feb-2018 |
immler <none@none> |
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
|
#
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
|
#
d463f754 |
|
19-Feb-2018 |
paulson <lp15@cam.ac.uk> |
lots of new material, ultimately related to measure theory
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
50836460 |
|
04-Dec-2017 |
Manuel Eberl <eberlm@in.tum.de> |
Moved material from AFP to Analysis/Number_Theory --HG-- extra : amend_source : 77bbfc2e280a37511c491c48def2d0c01459e12c
|
#
5c09067f |
|
09-Oct-2017 |
paulson <lp15@cam.ac.uk> |
new material about connectedness, etc.
|
#
bfd02107 |
|
14-Aug-2017 |
paulson <lp15@cam.ac.uk> |
patching the previous commit
|
#
5a58473a |
|
14-Aug-2017 |
paulson <lp15@cam.ac.uk> |
further Hensock tidy-up
|
#
7f0566a2 |
|
15-Jun-2017 |
paulson <lp15@cam.ac.uk> |
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
|
#
3f3e576c |
|
02-May-2017 |
paulson <lp15@cam.ac.uk> |
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
|
#
44a98e21 |
|
26-Apr-2017 |
paulson <lp15@cam.ac.uk> |
Further new material. The simprule status of some exp and ln identities was reverted.
|
#
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
|
#
97063f35 |
|
21-Feb-2017 |
paulson <lp15@cam.ac.uk> |
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
|
#
524cc9a4 |
|
05-Jan-2017 |
paulson <lp15@cam.ac.uk> |
New material about path connectedness, etc.
|
#
593ff4b4 |
|
17-Oct-2016 |
nipkow <none@none> |
setprod -> prod
|
#
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
#
7cb68da2 |
|
16-Oct-2016 |
haftmann <none@none> |
more standardized names
|
#
657eacc4 |
|
30-Sep-2016 |
paulson <lp15@cam.ac.uk> |
new material on paths, etc. Also rationalisation
|
#
8da99b63 |
|
21-Sep-2016 |
paulson <lp15@cam.ac.uk> |
vector_add_divide_simps now a "named theorems" bundle
|
#
6d0b05b4 |
|
18-Sep-2016 |
wenzelm <none@none> |
tuned proofs;
|
#
9b9c2176 |
|
12-Aug-2016 |
wenzelm <none@none> |
more symbols;
|
#
892044d3 |
|
28-Jul-2016 |
immler <none@none> |
numerical bounds on pi
|
#
85f0d545 |
|
22-Jul-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.
|
#
b62d1fc6 |
|
24-May-2016 |
paulson <lp15@cam.ac.uk> |
renamings and new material
|
#
b5509112 |
|
23-May-2016 |
paulson <lp15@cam.ac.uk> |
Lots of new material for multivariate analysis
|
#
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def'; tuned comments;
|
#
0c62267a |
|
11-Apr-2016 |
paulson <lp15@cam.ac.uk> |
lots of new theorems for multivariate analysis
|
#
db1c38d3 |
|
15-Mar-2016 |
paulson <lp15@cam.ac.uk> |
rationalisation of theorem names esp about "real Archimedian" etc.
|
#
a402e114 |
|
07-Mar-2016 |
paulson <lp15@cam.ac.uk> |
new material to Blochj's theorem, as well as supporting lemmas
|
#
15ee6658 |
|
24-Feb-2016 |
paulson <lp15@cam.ac.uk> |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
#
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!
|
#
30fd351a |
|
08-Feb-2016 |
hoelzl <none@none> |
add type class for topological monoids --HG-- extra : rebase_source : bedca3d32972c3f447e37ac5aac3de5ac763b94b
|
#
a6f23363 |
|
17-Feb-2016 |
haftmann <none@none> |
generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
|
#
2baeab22 |
|
11-Jan-2016 |
paulson <none@none> |
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
|
#
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
|
#
8b08bf14 |
|
07-Jan-2016 |
paulson <none@none> |
revisions to limits and derivatives, plus new lemmas
|
#
e68c51f7 |
|
04-Jan-2016 |
eberlm <none@none> |
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
|
#
322e58e3 |
|
30-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
#
82353fd1 |
|
30-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
#
6d3e0a15 |
|
29-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
#
ecc07c37 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "floor", "ceiling";
|
#
ba3fe537 |
|
23-Dec-2015 |
immler <none@none> |
transfer rule for bounded_linear of blinfun
|
#
f0118847 |
|
22-Dec-2015 |
immler <none@none> |
theory for type of bounded linear functions; differentiation under the integral sign
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
4b76bc27 |
|
01-Dec-2015 |
paulson <lp15@cam.ac.uk> |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
#
420aaf4c |
|
12-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
#
3f106d8a |
|
10-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
#
dd88f1ec |
|
02-Nov-2015 |
eberlm <none@none> |
Rounding function, uniform limits, cotangent, binomial identities
|
#
2f29d214 |
|
29-Oct-2015 |
eberlm <none@none> |
added many small lemmas about setsum/setprod/powr/...
|
#
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
#
78ffd573 |
|
31-Aug-2015 |
wenzelm <none@none> |
prefer symbols;
|
#
b63700d0 |
|
27-Jul-2015 |
paulson <lp15@cam.ac.uk> |
New material for Cauchy's integral theorem
|
#
a219c2a1 |
|
20-Jul-2015 |
paulson <none@none> |
new material for multivariate analysis, etc.
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
7f5fa27d |
|
28-May-2015 |
paulson <lp15@cam.ac.uk> |
Convex hulls: theorems about interior, etc. And a few simple lemmas.
|
#
eb3596fa |
|
26-May-2015 |
paulson <none@none> |
New material about paths, and some lemmas
|
#
c94afc60 |
|
29-Apr-2015 |
paulson <lp15@cam.ac.uk> |
Tidying. Improved simplification for numerals, esp in exponents.
|
#
f6ceb34e |
|
12-Apr-2015 |
paulson <lp15@cam.ac.uk> |
Restored LIMSEQ_def as legacy binding. [The other changes are whitespace only.]
|
#
d6db773a |
|
11-Apr-2015 |
paulson <lp15@cam.ac.uk> |
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
|
#
ac517014 |
|
31-Mar-2015 |
haftmann <none@none> |
given up separate type classes demanding `inverse 0 = 0`
|
#
e7eb131a |
|
18-Mar-2015 |
paulson <lp15@cam.ac.uk> |
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
|
#
9c83ffad |
|
09-Mar-2015 |
paulson <lp15@cam.ac.uk> |
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
|
#
b5ab68e6 |
|
05-Mar-2015 |
paulson <lp15@cam.ac.uk> |
The function frac. Various lemmas about limits, series, the exp function, etc.
|
#
e54b5053 |
|
04-Mar-2015 |
nipkow <none@none> |
Removed the obsolete functions "natfloor" and "natceiling"
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
#
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
#
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
|
#
bf4e83d3 |
|
28-Jun-2014 |
haftmann <none@none> |
fact consolidation
|
#
58bacf58 |
|
18-Jun-2014 |
hoelzl <none@none> |
filters are easier to define with INF on filters. --HG-- extra : rebase_source : 5626307315d6be224d16a97b9160690f09c8e0d4
|
#
58c27ade |
|
17-Jun-2014 |
hoelzl <none@none> |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin --HG-- extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2
|
#
61aadd1e |
|
06-May-2014 |
hoelzl <none@none> |
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex. --HG-- extra : rebase_source : 899541490c73fe6897445f97dc2a5a3c929cf153
|
#
77b90a1d |
|
09-Apr-2014 |
hoelzl <none@none> |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
#
36a1e2cc |
|
03-Apr-2014 |
paulson <lp15@cam.ac.uk> |
removing simprule status for divide_minus_left and divide_minus_right
|
#
3c2af176 |
|
02-Apr-2014 |
hoelzl <none@none> |
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
|
#
d6283f3b |
|
18-Mar-2014 |
hoelzl <none@none> |
fix HOL-NSA; move lemmas
|
#
9a3670d8 |
|
24-Feb-2014 |
paulson <lp15@cam.ac.uk> |
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
|
#
e93b90ff |
|
31-Dec-2013 |
haftmann <none@none> |
fundamental treatment of undefined vs. universally partial replaces code_abort
|
#
ac866a0f |
|
25-Dec-2013 |
haftmann <none@none> |
prefer more canonical names for lemmas on min/max
|
#
6f7f8de1 |
|
16-Dec-2013 |
immler <none@none> |
lemmas about divideR and scaleR
|
#
45834aba |
|
16-Dec-2013 |
immler <none@none> |
introduced ordered real vector spaces
|
#
b9995ead |
|
08-Dec-2013 |
wenzelm <none@none> |
more antiquotations;
|
#
138816de |
|
19-Nov-2013 |
haftmann <none@none> |
eliminiated neg_numeral in favour of - (numeral _)
|
#
839a96d8 |
|
05-Nov-2013 |
hoelzl <none@none> |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices) --HG-- rename : src/HOL/Library/Glbs.thy => src/HOL/Library/Lubs_Glbs.thy
|
#
d2ef840a |
|
01-Nov-2013 |
haftmann <none@none> |
more simplification rules on unary and binary minus --HG-- extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1
|
#
9de43fa6 |
|
12-Sep-2013 |
huffman <none@none> |
make 'linear' into a sublocale of 'bounded_linear'; replace 'linear_def' with 'linear_iff'
|
#
d7cd41cb |
|
03-Sep-2013 |
wenzelm <none@none> |
tuned proofs -- less guessing;
|
#
7237bdd9 |
|
02-Sep-2013 |
wenzelm <none@none> |
tuned proofs -- clarified flow of facts wrt. calculation;
|
#
e47024f1 |
|
15-Jun-2013 |
haftmann <none@none> |
pragmatic executability for instance real :: open
|
#
812b19ed |
|
25-Apr-2013 |
hoelzl <none@none> |
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
|
#
10810156 |
|
25-Apr-2013 |
hoelzl <none@none> |
renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS) --HG-- extra : rebase_source : 63f5230a997c030fcaa8377e299f12c9d6ec02a6
|
#
ad30da05 |
|
09-Apr-2013 |
hoelzl <none@none> |
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
|
#
4a0d6c03 |
|
09-Apr-2013 |
hoelzl <none@none> |
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
|
#
094b0ff5 |
|
25-Mar-2013 |
hoelzl <none@none> |
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
|
#
27fa2faa |
|
25-Mar-2013 |
hoelzl <none@none> |
rename RealVector.thy to Real_Vector_Spaces.thy --HG-- rename : src/HOL/RealVector.thy => src/HOL/Real_Vector_Spaces.thy
|