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