src/HOL/Library/Formal_Power_Series.thy
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-25 wenzelm 2013-08-25 tuned proofs;
2013-08-25 wenzelm 2013-08-25 tuned proofs;
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-08-07 wenzelm 2013-08-07 tuned proofs;
2013-08-07 wenzelm 2013-08-07 tuned proofs;
2013-08-07 wenzelm 2013-08-07 tuned proofs;
2013-03-26 wenzelm 2013-03-26 tuned imports;
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2013-02-13 immler 2013-02-13 complete metric for formal power series
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-08-10 wenzelm 2012-08-10 tuned proofs;
2012-03-30 huffman 2012-03-30 removed redundant nat-specific copies of theorems
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-02 bulwahn 2012-03-02 removing finiteness goals
2012-01-06 haftmann 2012-01-06 prefer listsum over foldl plus 0
2011-08-12 huffman 2011-08-12 make more HOL theories work with separate set type
2011-03-13 wenzelm 2011-03-13 tuned headers;
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-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
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-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-04-23 haftmann 2010-04-23 epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
2010-04-23 haftmann 2010-04-23 epheremal replacement of field_simps by field_eq_simps
2010-02-17 huffman 2010-02-17 fix more looping simp rules
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-08-31 nipkow 2009-08-31 tuned the simp rules for Int involving insert and intervals.
2009-08-26 chaieb 2009-08-26 merged
2009-05-19 chaieb 2009-05-19 merged
2009-05-19 chaieb 2009-05-19 Derivative of general reverses
2009-07-23 chaieb 2009-07-23 fixed proof --- fact_setprod removed for fact_altdef_nat
2009-07-23 chaieb 2009-07-23 merged
2009-07-23 chaieb 2009-07-23 Vandermonde vs Pochhammer; Hypergeometric series - very basic facts
2009-07-15 chaieb 2009-07-15 Moved important theorems from FPS_Examples to FPS --- they are not really examples but useful theorems that are being reproved since unnoticed.
2009-07-17 avigad 2009-07-17 Changed fact_Suc_nat back to fact_Suc
2009-07-14 avigad 2009-07-14 Repairs regarding new Fact.thy.
2009-07-09 chaieb 2009-07-09 FPS form a metric space, which justifies the infinte sum notation
2009-06-24 nipkow 2009-06-24 corrected and unified thm names
2009-06-23 haftmann 2009-06-23 simplified proof
2009-06-02 chaieb 2009-06-02 merged
2009-06-01 chaieb 2009-06-01 Reverses idempotent; radical of E; generalized logarithm;
2009-05-28 huffman 2009-05-28 addition formulas for fps_sin, fps_cos
2009-05-28 huffman 2009-05-28 use class field_char_0 for fps definitions
2009-05-18 chaieb 2009-05-18 FPS composition distributes over inverses, division and arbitrary nth roots. General geometric series theorem
2009-05-14 nipkow 2009-05-14 Cleaned up Parity a little
2009-05-08 chaieb 2009-05-08 fixed theorem statement
2009-05-08 chaieb 2009-05-08 Generalized distributivity theorems of radicals over multiplication, division and inverses
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-26 chaieb 2009-04-26 merged
2009-04-24 chaieb 2009-04-24 more general statements
2009-04-24 haftmann 2009-04-24 funpow and relpow with shared "^^" syntax
2009-04-22 haftmann 2009-04-22 power operation defined generic
2009-04-20 haftmann 2009-04-20 power operation on functions with syntax o^; power operation on relations with syntax ^^
2009-04-01 nipkow 2009-04-01 added strong_setprod_cong[cong] (in analogy with setsum) added some lemmas
2009-03-27 chaieb 2009-03-27 merged
2009-03-27 chaieb 2009-03-27 fps made instance of number_ring