--- 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
--- 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
--- a/doc-src/TutorialI/ToyList/ToyList.thy Fri May 31 07:55:17 2002 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Fri May 31 09:50:16 2002 +0200
@@ -33,7 +33,7 @@
The @{text 65} is the priority of the infix @{text"#"}.
\begin{warn}
- Syntax annotations are can be powerful, but they are difficult to master and
+ Syntax annotations can be powerful, but they are difficult to master and
are never necessary. You
could drop them from theory @{text"ToyList"} and go back to the identifiers
@{term[source]Nil} and @{term[source]Cons}.
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Fri May 31 07:55:17 2002 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Fri May 31 09:50:16 2002 +0200
@@ -38,7 +38,7 @@
The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
\begin{warn}
- Syntax annotations are can be powerful, but they are difficult to master and
+ Syntax annotations can be powerful, but they are difficult to master and
are never necessary. You
could drop them from theory \isa{ToyList} and go back to the identifiers
\isa{Nil} and \isa{Cons}.