src/HOL/Library/Formal_Power_Series.thy
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-02-14 huffman 2009-02-14 generalize lemma fps_square_eq_iff, move to Ring_and_Field
2009-02-14 huffman 2009-02-14 generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
2009-02-14 huffman 2009-02-14 add mult_delta lemmas; simplify some proofs
2009-02-14 huffman 2009-02-14 fix spelling
2009-02-14 huffman 2009-02-14 declare fps_nth as a typedef morphism; clean up instance proofs
2009-02-13 huffman 2009-02-13 section -> subsection
2009-01-29 berghofe 2009-01-29 Enclosed name containing _'s in @{text ...} antiquotation to make document preparation work again.
2009-01-29 chaieb 2009-01-29 removed definition of funpow , reusing that of Relation_Power
2009-01-29 chaieb 2009-01-29 A formalization of formal power series