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/Hyperreal/Transcendental.ML
changeset 15053 405be2b48f5b
parent 15047 fa62de5862b9 
--- a/src/HOL/Hyperreal/Transcendental.ML	Fri Jul 16 11:46:59 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.ML	Fri Jul 16 17:31:44 2004 +0200
@@ -394,8 +394,6 @@
 (* Properties of power series                                               *)
 (*--------------------------------------------------------------------------*)
 
-Delsimps [thm"atLeast0LessThan"];
-
 Goal "sumr 0 (Suc n) (%p. (x ^ p) * y ^ ((Suc n) - p)) = \
 \     y * sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p)))";
 by (auto_tac (claset(),simpset() addsimps [sumr_mult] delsimps [sumr_Suc]));
isabelle