--- 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}.