src/HOL/Computational_Algebra/Formal_Power_Series.thy
19 months ago haftmann 2017-10-08 euclidean rings need no normalization
19 months ago haftmann 2017-10-08 abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
19 months ago haftmann 2017-10-08 avoid name clashes on interpretation of abstract locales
21 months ago eberlm 2017-08-29 Some small lemmas about polynomials and FPSs
21 months ago Manuel Eberl 2017-08-21 HOL-Analysis: Convergent FPS and infinite sums
21 months ago Manuel Eberl 2017-08-20 More lemmas for HOL-Analysis
22 months ago eberlm 2017-08-03 Removed unnecessary constant 'ball' from Formal_Power_Series
22 months ago nipkow 2017-08-03 added lemmas
23 months ago paulson 2017-06-15 Some new material. SIMPRULE STATUS for sum/prod.delta rules!
2017-04-25 paulson 2017-04-25 New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
2017-04-07 wenzelm 2017-04-07 tuned headers;
2017-04-06 haftmann 2017-04-06 session containing computational algebra