# HG changeset patch
# User nipkow
# Date 1022831416 -7200
# Node ID 05a9929ee10eede3928ae4aa66c494071a140d3c
# Parent  172f65d0c3d1fb2a9c8529f9000c3576d8c14c3a
*** empty log message ***

diff -r 172f65d0c3d1 -r 05a9929ee10e doc-src/TutorialI/Advanced/document/simp.tex
--- 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
diff -r 172f65d0c3d1 -r 05a9929ee10e doc-src/TutorialI/Advanced/simp.thy
--- 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
diff -r 172f65d0c3d1 -r 05a9929ee10e doc-src/TutorialI/ToyList/ToyList.thy
--- 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}.
diff -r 172f65d0c3d1 -r 05a9929ee10e doc-src/TutorialI/ToyList/document/ToyList.tex
--- 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}.