| 6 months ago |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| 12 months ago |
paulson |
New material from a variety of sources (including AFP)
|
file |
diff |
annotate
|
| 12 months ago |
paulson |
New material by Wenda Li and Manuel Eberl
|
file |
diff |
annotate
|
| 20 months ago |
paulson |
substantial tidy-up, shortening many proofs
|
file |
diff |
annotate
|
| 2023-02-09 |
paulson |
More material for Analysis and Complex_Analysis
|
file |
diff |
annotate
|
| 2023-02-06 |
paulson |
Some more new material and some tidying of existing proofs
|
file |
diff |
annotate
|
| 2023-02-01 |
paulson |
More new material thanks to Manuel
|
file |
diff |
annotate
|
| 2022-03-01 |
paulson |
Added some theorems (from Wetzel)
|
file |
diff |
annotate
|
| 2021-10-15 |
paulson |
A few new lemmas plus some refinements
|
file |
diff |
annotate
|
| 2021-06-28 |
paulson |
A few useful lemmas about derivatives, colinearity and other topics
|
file |
diff |
annotate
|
| 2020-03-31 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| 2019-11-30 |
Manuel Eberl |
Split off new HOL-Complex_Analysis session from HOL-Analysis
|
file |
diff |
annotate
|
| 2019-11-26 |
paulson |
Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.
|
file |
diff |
annotate
|
| 2019-11-05 |
paulson |
Merge and get rid of closed_segmentI
|
file |
diff |
annotate
|
| 2019-11-04 |
paulson |
Moved or deleted some out of place material, also eliminating obsolete naming conventions
|
file |
diff |
annotate
|
| 2019-11-02 |
paulson |
reorganisation to eliminate Brouwer_Fixpoint from complex analysis
|
file |
diff |
annotate
|
| 2019-10-09 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| 2019-09-16 |
paulson |
A little-known material, and some tidying up
|
file |
diff |
annotate
|
| 2019-08-27 |
immler |
removed Brouwer_Fixpoint from imports of Derivative
|
file |
diff |
annotate
|
| 2019-04-26 |
paulson |
Added embedding_map_into_euclideanreal; reduced dependence on Equivalence_Lebesgue_Henstock_Integration in Analysis theories by moving a few lemmas
|
file |
diff |
annotate
|
| 2019-04-12 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| 2018-12-29 |
nipkow |
capitalize proper names in lemma names
|
file |
diff |
annotate
|
| 2018-12-27 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
| 2018-11-11 |
nipkow |
tuned
|
file |
diff |
annotate
|
| 2018-10-22 |
Manuel Eberl |
Tagged some theories in HOL-Analysis
|
file |
diff |
annotate
|
| 2018-09-24 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| 2018-08-03 |
eberlm |
Small lemmas about analysis
|
file |
diff |
annotate
|
| 2018-05-26 |
paulson |
tidying and reorganisation around Cauchy Integral Theorem
|
file |
diff |
annotate
|
| 2018-05-21 |
paulson |
small clean-up of Complex_Analysis_Basics
|
file |
diff |
annotate
|
| 2018-05-20 |
paulson |
tidy up of Derivative
|
file |
diff |
annotate
|
| 2018-04-29 |
paulson |
more defer/prefer
|
file |
diff |
annotate
|
| 2018-04-14 |
paulson |
new material about vec, real^1, etc.
|
file |
diff |
annotate
|
| 2018-04-09 |
nipkow |
removed dots at the end of (sub)titles
|
file |
diff |
annotate
|
| 2018-01-10 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| 2018-01-08 |
paulson |
moved in some material from Euler-MacLaurin
|
file |
diff |
annotate
|
| 2017-12-12 |
Manuel Eberl |
Moved analysis material from AFP
|
file |
diff |
annotate
|
| 2017-12-05 |
Manuel Eberl |
Moved material from AFP to Analysis/Number_Theory
|
file |
diff |
annotate
|
| 2017-10-10 |
paulson |
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
|
file |
diff |
annotate
|
| 2017-08-22 |
Manuel Eberl |
Lemmas about analysis and permutations
|
file |
diff |
annotate
|
| 2017-08-18 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| 2017-07-04 |
immler |
some generalizations complex=>real_normed_field
|
file |
diff |
annotate
|
| 2017-06-15 |
paulson |
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
|
file |
diff |
annotate
|
| 2017-04-27 |
paulson |
New material (and some tidying) purely in the Analysis directory
|
file |
diff |
annotate
|
| 2016-10-25 |
paulson |
more new material
|
file |
diff |
annotate
|
| 2016-10-17 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| 2016-09-23 |
hoelzl |
move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
|
file |
diff |
annotate
|
| 2016-09-19 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
| 2016-09-16 |
hoelzl |
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
|
file |
diff |
annotate
|
| 2016-08-08 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
| base
|