src/HOL/Library/Formal_Power_Series.thy
changeset 30746 d6915b738bd9
parent 30488 5c4c3a9e9102
child 30747 b8ca7e450de3
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Mar 19 22:05:37 2009 +0100
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Mar 27 14:43:47 2009 +0000
     1.3 @@ -389,6 +389,14 @@
     1.4  
     1.5  instance fps :: (idom) idom ..
     1.6  
     1.7 +instantiation fps :: (comm_ring_1) number_ring
     1.8 +begin
     1.9 +definition number_of_fps_def: "(number_of k::'a fps) = of_int k"
    1.10 +
    1.11 +instance 
    1.12 +by (intro_classes, rule number_of_fps_def)
    1.13 +end
    1.14 +
    1.15  subsection{* Inverses of formal power series *}
    1.16  
    1.17  declare setsum_cong[fundef_cong]