src/HOL/Filter.thy
2016-06-22 wenzelm 2016-06-22 bundle lifting_syntax;
2016-02-22 paulson 2016-02-22 An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
2016-02-19 hoelzl 2016-02-19 generalize more theorems to support enat and ennreal
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-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
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-28 wenzelm 2015-12-28 use symbols by default;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
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-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-09-25 hoelzl 2015-09-25 prove Liminf_inverse_ereal
2015-09-22 paulson 2015-09-22 Prepared two non-terminating proofs; no obvious link with my changes
2015-08-19 paulson 2015-08-19 New material and fixes related to the forthcoming Stone-Weierstrass development
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-14 hoelzl 2015-07-14 generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
2015-06-26 wenzelm 2015-06-26 do not expose goal parameters;
2015-05-07 hoelzl 2015-05-07 generalized tends over powr; added DERIV rule for powr
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 add cofinite filter
2015-04-12 hoelzl 2015-04-12 add frequently as dual for eventually
2015-04-12 hoelzl 2015-04-12 add quantifier syntax for eventually
2015-04-12 hoelzl 2015-04-12 move filters to their own theory