src/HOL/Library/Formal_Power_Series.thy
2010-06-08 ago tuned quotes, antiquotations and whitespace
2010-05-11 ago 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 ago theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
2010-04-26 ago use new classes (linordered_)field_inverse_zero
2010-04-26 ago dropped group_simps, ring_simps, field_eq_simps
2010-04-23 ago epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
2010-04-23 ago epheremal replacement of field_simps by field_eq_simps
2010-02-17 ago fix more looping simp rules
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-08-31 ago tuned the simp rules for Int involving insert and intervals.
2009-08-26 ago merged
2009-05-19 ago merged
2009-05-19 ago Derivative of general reverses
2009-07-23 ago fixed proof --- fact_setprod removed for fact_altdef_nat
2009-07-23 ago merged
2009-07-23 ago Vandermonde vs Pochhammer; Hypergeometric series - very basic facts
2009-07-15 ago Moved important theorems from FPS_Examples to FPS --- they are not
2009-07-17 ago Changed fact_Suc_nat back to fact_Suc
2009-07-14 ago Repairs regarding new Fact.thy.
2009-07-09 ago FPS form a metric space, which justifies the infinte sum notation
2009-06-24 ago corrected and unified thm names
2009-06-23 ago simplified proof
2009-06-02 ago merged
2009-06-01 ago Reverses idempotent; radical of E; generalized logarithm;
2009-05-28 ago addition formulas for fps_sin, fps_cos
2009-05-28 ago use class field_char_0 for fps definitions
2009-05-18 ago FPS composition distributes over inverses, division and arbitrary nth roots. General geometric series theorem
2009-05-14 ago Cleaned up Parity a little
2009-05-08 ago fixed theorem statement
2009-05-08 ago Generalized distributivity theorems of radicals over multiplication, division and inverses
2009-04-29 ago farewell to class recpower
2009-04-26 ago merged
2009-04-24 ago more general statements
2009-04-24 ago funpow and relpow with shared "^^" syntax
2009-04-22 ago power operation defined generic
2009-04-20 ago power operation on functions with syntax o^; power operation on relations with syntax ^^
2009-04-01 ago added strong_setprod_cong[cong] (in analogy with setsum)
2009-03-27 ago merged
2009-03-27 ago fps made instance of number_ring
2009-03-23 ago tuned header
2009-03-12 ago remove trailing spaces
2009-03-04 ago declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-02-14 ago generalize lemma fps_square_eq_iff, move to Ring_and_Field
2009-02-14 ago generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
2009-02-14 ago add mult_delta lemmas; simplify some proofs
2009-02-14 ago fix spelling
2009-02-14 ago declare fps_nth as a typedef morphism; clean up instance proofs
2009-02-13 ago section -> subsection
2009-01-29 ago Enclosed name containing _'s in @{text ...} antiquotation to make document
2009-01-29 ago removed definition of funpow , reusing that of Relation_Power
2009-01-29 ago A formalization of formal power series