--- a/doc-src/TutorialI/Advanced/document/simp.tex Fri May 31 07:55:17 2002 +0200
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Fri May 31 09:50:16 2002 +0200
@@ -26,7 +26,7 @@
\begin{isamarkuptext}%
\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, \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ xs\ {\isacharat}\ xs\ {\isacharequal}\ xs} simplifies to \isa{True} because we may use \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} when simplifying \isa{xs\ {\isacharat}\ xs\ {\isacharequal}\ xs}. The generation of contextual information during simplification is