src/HOL/Topological_Spaces.thy
2017-03-10 immler 2017-03-10 modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
2017-02-21 paulson 2017-02-21 Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
2017-01-31 eberlm 2017-01-31 Simplified Gamma_Function
2017-01-09 paulson 2017-01-09 Advanced topology
2017-01-04 paulson 2017-01-04 Many new theorems, and more tidying
2017-01-03 paulson 2017-01-03 A few new lemmas and needed adaptations
2016-10-25 paulson 2016-10-25 more new material
2016-10-18 hoelzl 2016-10-18 HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
2016-10-13 hoelzl 2016-10-13 HOL-Probability: move conditional expectation from AFP/Ergodic_Theory
2016-09-30 hoelzl 2016-09-30 HOL-Probability: more about probability, prepare for Markov processes in the AFP
2016-09-28 paulson 2016-09-28 new material connected with HOL Light measure theory, plus more rationalisation
2016-08-17 eberlm 2016-08-17 Tuned L'Hospital
2016-07-15 wenzelm 2016-07-15 proper latex;
2016-07-15 wenzelm 2016-07-15 misc tuning and modernization;
2016-06-15 hoelzl 2016-06-15 move open_Collect_eq/less to HOL
2016-06-16 eberlm 2016-06-16 Various additions to polynomials, FPSs, Gamma function
2016-06-14 paulson 2016-06-14 new results about topology
2016-06-13 eberlm 2016-06-13 Facts about HK integration, complex powers, Gamma function
2016-05-27 wenzelm 2016-05-27 tuned proofs;
2016-05-27 wenzelm 2016-05-27 tuned proofs, to allow unfold_abs_def;
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