src/HOL/ex/Summation.thy
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-05-11 haftmann 2010-05-11 renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
2010-05-11 haftmann 2010-05-11 theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
2010-03-11 haftmann 2010-03-11 tuned prefix of ac rules
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-02-17 haftmann 2010-02-17 added simple theory about discrete summation