--- a/doc-src/TutorialI/Advanced/simp.thy Fri May 31 07:55:17 2002 +0200
+++ b/doc-src/TutorialI/Advanced/simp.thy Fri May 31 09:50:16 2002 +0200
@@ -16,7 +16,7 @@
text{*\label{sec:simp-cong}
While simplifying the conclusion $Q$
-of $P \Imp Q$, it is legal use the assumption $P$.
+of $P \Imp Q$, it is legal to use the assumption $P$.
For $\Imp$ this policy is hardwired, but
contextual information can also be made available for other
operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term