We stress the need to have a proper semantics for computer algebra expressions, especially if one wants to use results and methods from computer algebra in theorem provers. The computer algebra method under discussion in this paper is the use of rewrite rules to evaluate limits involving infinity.