src/HOL/Topological_Spaces.thy
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)
2014-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-03-31 hoelzl 2014-03-31 add connected_local_const
2014-03-26 paulson 2014-03-26 Some useful lemmas
2014-03-20 wenzelm 2014-03-20 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-10 hoelzl 2014-03-10 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-06 blanchet 2014-03-06 renamed 'filter_rel' to 'rel_filter'
2014-03-06 blanchet 2014-03-06 renamed 'set_rel' to 'rel_set'
2014-02-27 paulson 2014-02-27 A bit of tidying up
2014-02-25 paulson 2014-02-25 More complex-related lemmas
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-18 kuncar 2014-02-18 delete or move now not necessary reflexivity rules due to 1726f46d2aa8