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