2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-04-18 paulson 2016-04-18 new theorems about convex hulls, etc.; also, renamed some theorems
2016-04-04 paulson 2016-04-04 Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
2016-03-07 paulson 2016-03-07 new material to Blochj's theorem, as well as supporting lemmas
2016-02-24 paulson 2016-02-24 Substantial new material for multivariate analysis. Also removal of some duplicates.
2016-02-23 paulson 2016-02-23 New and revised material for (multivariate) analysis
2016-02-09 hoelzl 2016-02-09 instantiate topologies for nat, int and enat
2016-02-08 hoelzl 2016-02-08 move product topology to HOL-Complex_Main
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-01-22 paulson 2016-01-22 Reorganised a huge proof
2016-01-13 wenzelm 2016-01-13 isabelle update_cartouches -c -t;
2016-01-11 hoelzl 2016-01-11 setup code generation for filters as suggested by Florian
2016-01-08 hoelzl 2016-01-08 fix code generation for uniformity: uniformity is a non-computable pure data.
2016-01-08 hoelzl 2016-01-08 add uniform spaces
2016-01-06 hoelzl 2016-01-06 add the proof of the central limit theorem
2016-01-04 eberlm 2016-01-04 Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-22 paulson 2015-12-22 Liouville theorem, Fundamental Theorem of Algebra, etc.
2015-12-09 paulson 2015-12-09 sorted out eventually_mono
2015-12-07 paulson 2015-12-07 Cauchy's integral formula for circles. Starting to fix eventually_mono.
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-23 paulson 2015-11-23 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
2015-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-10-27 paulson 2015-10-27 Cauchy's integral formula, required lemmas, and a bit of reorganisation
2015-10-13 paulson 2015-10-13 new material on path_component_sets, inside, outside, etc. And more default simprules
2015-10-06 wenzelm 2015-10-06 isabelle update_cartouches;
2015-10-02 paulson 2015-10-02 New theorems about connected sets. And pairwise moved to Set.thy.
2015-09-25 hoelzl 2015-09-25 prove Liminf_inverse_ereal
2015-09-22 paulson 2015-09-22 New lemmas
2015-09-21 paulson 2015-09-21 new lemmas and movement of lemmas into place
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-07-20 paulson 2015-07-20 new material for multivariate analysis, etc.
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-14 hoelzl 2015-07-14 add continuous_onI_mono
2015-06-26 wenzelm 2015-06-26 tuned whitespace;
2015-05-07 hoelzl 2015-05-07 generalized tends over powr; added DERIV rule for powr
2015-05-04 hoelzl 2015-05-04 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
2015-04-28 paulson 2015-04-28 New material about complex transcendental functions (especially Ln, Arg) and polynomials
2015-04-12 hoelzl 2015-04-12 move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
2015-04-12 hoelzl 2015-04-12 move filters to their own theory
2015-04-08 wenzelm 2015-04-08 more standard access to goal state;
2015-04-08 wenzelm 2015-04-08 tuned signature;
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-01-27 hoelzl 2015-01-27 ereal: tuned proofs concerning continuity and suprema
2014-12-08 hoelzl 2014-12-08 instance bool and enat as topologies
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-20 hoelzl 2014-10-20 add tendsto_const and tendsto_ident_at as simp and intro rules
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-06-30 hoelzl 2014-06-30 more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-06-18 hoelzl 2014-06-18 filters are easier to define with INF on filters.
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-05-20 hoelzl 2014-05-20 add various lemmas
2014-05-13 hoelzl 2014-05-13 clean up Lebesgue integration
2014-04-10 kuncar 2014-04-10 setup for Transfer and Lifting from BNF; tuned thm names
2014-04-10 kuncar 2014-04-10 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)