diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Advanced/simp.thy
--- a/doc-src/TutorialI/Advanced/simp.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/simp.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -17,7 +17,7 @@
 
 text{*\label{sec:simp-cong}
 It is hardwired into the simplifier that while simplifying the conclusion $Q$
-of $P \isasymImp Q$ it is legal to make uses of the assumptions $P$. This
+of $P \Imp Q$ it is legal to make uses of the assumption $P$. This
 kind of contextual information can also be made available for other
 operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term
 True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs =
@@ -33,8 +33,8 @@
 Here are some more examples.  The congruence rules for bounded
 quantifiers supply contextual information about the bound variable:
 @{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
-The congruence rule for conditional expressions supply contextual
-information for simplifying the arms:
+The congruence rule for conditional expressions supplies contextual
+information for simplifying the @{text then} and @{text else} cases:
 @{thm[display]if_cong[no_vars]}
 A congruence rule can also \emph{prevent} simplification of some arguments.
 Here is an alternative congruence rule for conditional expressions:
@@ -42,7 +42,7 @@
 Only the first argument is simplified; the others remain unchanged.
 This makes simplification much faster and is faithful to the evaluation
 strategy in programming languages, which is why this is the default
-congruence rule for @{text if}. Analogous rules control the evaluaton of
+congruence rule for @{text if}. Analogous rules control the evaluation of
 @{text case} expressions.
 
 You can declare your own congruence rules with the attribute @{text cong},
@@ -107,7 +107,7 @@
 
 Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely
 necessary because the built-in arithmetic prover often succeeds without
-such hints.
+such tricks.
 *}
 
 subsection{*How It Works*}
@@ -149,8 +149,7 @@
 ?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is fine
 as a conditional rewrite rule since conditions can be arbitrary
 terms. However, this trick is not a panacea because the newly
-introduced conditions may be hard to prove, as they must be
-before the rule can actually be applied.
+introduced conditions may be hard to solve.
   
 There is no restriction on the form of the right-hand
 sides.  They may not contain extraneous term or type variables, though.