src/HOL/Library/SetsAndFunctions.thy
2009-03-27 haftmann 2009-03-27 merged
2009-03-27 haftmann 2009-03-27 normalized imports
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
2008-12-14 ballarin 2008-12-14 Ported HOL and HOL-Library to new locales.
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.
2008-01-02 haftmann 2008-01-02 removed some legacy instantiations
2007-12-18 haftmann 2007-12-18 switched from PreList to ATP_Linkup
2007-12-10 haftmann 2007-12-10 switched import from Main to PreList
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-09-13 krauss 2006-09-13 Major update to function package, including new syntax and the (only theoretical) ability to handle local contexts.
2006-05-27 wenzelm 2006-05-27 tuned;
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-04-09 wenzelm 2006-04-09 tuned syntax/abbreviations;
2005-08-28 wenzelm 2005-08-28 tuned some proofs;
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