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