src/HOL/Computational_Algebra/Formal_Power_Series.thy
10 months ago nipkow 2018-06-14 tuned
11 months ago immler 2018-05-02 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
12 months ago paulson 2018-04-09 A couple of new results
15 months ago haftmann 2018-01-13 restored naming of lemmas after corresponding constants
15 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
18 months ago haftmann 2017-10-08 euclidean rings need no normalization
18 months ago haftmann 2017-10-08 abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
18 months ago haftmann 2017-10-08 avoid name clashes on interpretation of abstract locales
19 months ago eberlm 2017-08-29 Some small lemmas about polynomials and FPSs
20 months ago Manuel Eberl 2017-08-21 HOL-Analysis: Convergent FPS and infinite sums
20 months ago Manuel Eberl 2017-08-20 More lemmas for HOL-Analysis
20 months ago eberlm 2017-08-03 Removed unnecessary constant 'ball' from Formal_Power_Series
20 months ago nipkow 2017-08-03 added lemmas
22 months ago paulson 2017-06-15 Some new material. SIMPRULE STATUS for sum/prod.delta rules!
24 months ago 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