src/HOL/Library/Formal_Power_Series.thy
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
2009-03-23 haftmann 2009-03-23 tuned header
2009-03-12 huffman 2009-03-12 remove trailing spaces
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