Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Formal_Power_Series.thy
changeset 31075 a9d6cf6de9a8
parent 31073 4b44c4d08aa6
child 31148 7ba7c1f8bc22
child 32410 624bd2ea7c1e 
--- 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