Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed theorem statement
authorchaieb
Fri, 08 May 2009 19:28:11 +0100
changeset 31075 a9d6cf6de9a8
parent 31074 710cd642650e
child 31076 99fe356cbbc2
fixed theorem statement
src/HOL/Library/Formal_Power_Series.thy file | annotate | diff | comparison | revisions 
--- 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")
isabelle