# HG changeset patch
# User chaieb
# Date 1238165027 0
# Node ID d6915b738bd95a8dddf655d8ab7435303524daad
# Parent  4216e9c70cfe6766df47dcc54926fd46964bfd8d
fps made instance of number_ring

diff -r 4216e9c70cfe -r d6915b738bd9 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Thu Mar 19 22:05:37 2009 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Mar 27 14:43:47 2009 +0000
@@ -389,6 +389,14 @@
 
 instance fps :: (idom) idom ..
 
+instantiation fps :: (comm_ring_1) number_ring
+begin
+definition number_of_fps_def: "(number_of k::'a fps) = of_int k"
+
+instance 
+by (intro_classes, rule number_of_fps_def)
+end
+
 subsection{* Inverses of formal power series *}
 
 declare setsum_cong[fundef_cong]