src/HOL/Library/BigO.thy
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-04-22 paulson 2015-04-22 fixes for limits
2015-04-21 paulson 2015-04-21 New material, mostly about limits. Consolidation.
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-07 wenzelm 2014-10-07 more antiquotations;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-04-29 wenzelm 2014-04-29 tuned proofs;
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-03-01 wenzelm 2014-03-01 more symbols, less parentheses;
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2012-04-12 krauss 2012-04-12 Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-10-27 huffman 2011-10-27 fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
2011-04-08 wenzelm 2011-04-08 removed outdated text (cf. 84a3f86441eb);
2011-02-28 paulson 2011-02-28 declare ext [intro]: Extensionality now available by default
2011-01-12 wenzelm 2011-01-12 eliminated global prems; tuned proofs;
2010-08-20 haftmann 2010-08-20 split and enriched theory SetsAndFunctions
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-05-28 huffman 2009-05-28 LIMSEQ_def -> LIMSEQ_iff
2009-02-03 haftmann 2009-02-03 merged Big0
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-05-07 berghofe 2008-05-07 Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with definitions of + and * on functions.
2007-12-10 haftmann 2007-12-10 explicit import of theory Main
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-17 nipkow 2007-06-17 tuned laws for cancellation in divisions for fields.
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-04-13 wenzelm 2007-04-13 tuned document (headers, sections, spacing);
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-05-27 wenzelm 2006-05-27 tuned;
2006-03-17 ballarin 2006-03-17 Renamed setsum_mult to setsum_right_distrib.
2005-08-31 wenzelm 2005-08-31 moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy; tuned presentation;
2005-07-29 avigad 2005-07-29 fixed minor typo in comments
2005-07-28 wenzelm 2005-07-28 proper header;
2005-07-25 avigad 2005-07-25 Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy