fixed theorem statement
authorchaieb
Fri May 08 19:28:11 2009 +0100 (2009-05-08)
changeset 31075a9d6cf6de9a8
parent 31074 710cd642650e
child 31076 99fe356cbbc2
fixed theorem statement
src/HOL/Library/Formal_Power_Series.thy
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri May 08 14:03:24 2009 +0100
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri May 08 19:28:11 2009 +0100
     1.3 @@ -1758,7 +1758,6 @@
     1.4    kp: "k>0"
     1.5    and ra0: "(r k (a $ 0)) ^ k = a $ 0"
     1.6    and rb0: "(r k (b $ 0)) ^ k = b $ 0"
     1.7 -  and r1: "(r k 1)^k = 1"
     1.8    and a0: "a$0 \<noteq> 0"
     1.9    and b0: "b$0 \<noteq> 0"
    1.10    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")