merged
authorchaieb
Fri Mar 27 14:44:18 2009 +0000 (2009-03-27)
changeset 30747b8ca7e450de3
parent 30744 50ccaef52871
parent 30746 d6915b738bd9
child 30748 fe67d729a61c
child 30765 3eccfc8019ba
merged
src/HOL/Library/Formal_Power_Series.thy
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Mar 27 15:42:53 2009 +0100
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Mar 27 14:44:18 2009 +0000
     1.3 @@ -388,6 +388,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]