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