# HG changeset patch
# User chaieb
# Date 1241807291 -3600
# Node ID a9d6cf6de9a8f1b4a9fb3bc64293e9f85cd602c9
# Parent  710cd642650e7e4227184bbf2b8a29e71fc0edc8
fixed theorem statement

diff -r 710cd642650e -r a9d6cf6de9a8 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri May 08 14:03:24 2009 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri May 08 19:28:11 2009 +0100
@@ -1758,7 +1758,6 @@
   kp: "k>0"
   and ra0: "(r k (a $ 0)) ^ k = a $ 0"
   and rb0: "(r k (b $ 0)) ^ k = b $ 0"
-  and r1: "(r k 1)^k = 1"
   and a0: "a$0 \<noteq> 0"
   and b0: "b$0 \<noteq> 0"
   shows "r k ((a $ 0) / (b$0)) = r k (a$0) / r k (b $ 0) \<longleftrightarrow> fps_radical r k (a/b) = fps_radical r k a / fps_radical r k b" (is "?lhs = ?rhs")