5 months ago wenzelm 2019-01-05 isabelle update -u control_cartouches;
5 months ago wenzelm 2019-01-01 more antiquotations -- less LaTeX macros;
5 months ago nipkow 2018-12-29 capitalize proper names in lemma names
5 months ago nipkow 2018-12-27 tuned headers; ~ -> \<not>
8 months ago Manuel Eberl 2018-10-22 Tagged some theories in HOL-Analysis
10 months ago eberlm 2018-08-04 Small lemmas about analysis
11 months ago paulson 2018-07-03 more on infinite products
12 months ago paulson 2018-06-29 The unwinding number is an integer.
12 months ago paulson 2018-06-28 Generalising and renaming some basic results
12 months ago paulson 2018-06-26 a few new lemmas
12 months ago paulson 2018-06-26 Rationalisation of complex transcendentals, esp the Arg function
12 months ago paulson 2018-06-25 Renaming Arg -> Arg2pi
13 months ago paulson 2018-05-24 more small tidying
13 months ago paulson 2018-05-23 small tidy-up of Complex_Transcendental
13 months ago paulson 2018-05-21 small clean-up of Complex_Analysis_Basics
14 months ago paulson 2018-04-12 Analysis builds using set_borel_measurable_def, etc.
14 months ago nipkow 2018-04-09 removed dots at the end of (sub)titles
16 months ago Wenda Li 2018-02-23 Unified the order of zeros and poles; improved reasoning around non-essential singularites
16 months ago Manuel Eberl 2018-02-08 Some lemmas about complex sinh/cosh/tanh
17 months ago wenzelm 2018-01-16 standardized towards new-style formal comments: isabelle update_comments;
17 months ago paulson 2018-01-08 moved in some material from Euler-MacLaurin
18 months ago eberlm 2017-12-24 Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
18 months ago paulson 2017-12-22 new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
18 months ago Manuel Eberl 2017-12-05 Moved material from AFP to Analysis/Number_Theory
20 months ago paulson 2017-10-10 Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
20 months ago paulson 2017-10-09 new material about connectedness, etc.
21 months ago nipkow 2017-09-07 adapted to better linear arith
22 months ago Manuel Eberl 2017-08-21 HOL-Analysis: Convergent FPS and infinite sums
22 months ago Manuel Eberl 2017-08-20 More lemmas for HOL-Analysis
22 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
22 months ago eberlm 2017-08-17 Replaced subseq with strict_mono
24 months ago immler 2017-07-04 some generalizations complex=>real_normed_field
2017-05-04 paulson 2017-05-04 A few more new lemmas
2017-04-27 paulson 2017-04-27 New material (and some tidying) purely in the Analysis directory
2017-04-26 paulson 2017-04-26 Some fixes related to compactE_image
2017-04-26 paulson 2017-04-26 Further new material. The simprule status of some exp and ln identities was reverted.
2017-04-25 paulson 2017-04-25 New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
2017-03-16 paulson 2017-03-16 Removed [simp] status for Complex_eq. Also tidied some proofs
2017-02-28 paulson 2017-02-28 Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
2017-02-21 paulson 2017-02-21 Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
2017-01-05 paulson 2017-01-05 New theory of arcwise connected sets and other new material
2017-01-04 paulson 2017-01-04 Many new theorems, and more tidying
2016-12-17 haftmann 2016-12-17 reoriented congruence rules in non-explosive direction
2016-11-19 wenzelm 2016-11-19 more symbols;
2016-10-25 paulson 2016-10-25 more new material
2016-10-18 paulson 2016-10-18 more from
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-10-16 haftmann 2016-10-16 more standardized names
2016-09-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-08-25 Manuel Eberl 2016-08-25 More analysis lemmas
2016-08-08 hoelzl 2016-08-08 rename HOL-Multivariate_Analysis to HOL-Analysis.