diff -r e0ab13bec5c8 -r 166f7d87b37f doc-src/TutorialI/Advanced/WFrec.thy
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Tue Feb 20 11:27:04 2001 +0100
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Tue Feb 20 13:23:58 2001 +0100
@@ -1,7 +1,7 @@
 (*<*)theory WFrec = Main:(*>*)
 
 text{*\noindent
-So far, all recursive definitions where shown to terminate via measure
+So far, all recursive definitions were shown to terminate via measure
 functions. Sometimes this can be quite inconvenient or even
 impossible. Fortunately, \isacommand{recdef} supports much more
 general definitions. For example, termination of Ackermann's function