diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Inductive/AB.thy
--- a/doc-src/TutorialI/Inductive/AB.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -303,6 +303,6 @@
 similar to the other cases (which are automatic in Isabelle). We conclude
 that the authors are at least cavalier about this point and may even have
 overlooked the slight difficulty lurking in the omitted cases. This is not
-atypical for pen-and-paper proofs, once analysed in detail.  *}
+atypical for pencil-and-paper proofs, once analysed in detail.  *}
 
 (*<*)end(*>*)