# HG changeset patch
# User chaieb
# Date 1238165058 0
# Node ID b8ca7e450de36c897479274cf5d47507edefe485
# Parent  50ccaef52871f3532ab2f2f39b1088b144e8a3a0# Parent  d6915b738bd95a8dddf655d8ab7435303524daad
merged

diff -r 50ccaef52871 -r b8ca7e450de3 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Mar 27 15:42:53 2009 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Mar 27 14:44:18 2009 +0000
@@ -388,6 +388,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]