src/HOL/Filter.thy
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