--- a/doc-src/TutorialI/CTL/document/PDL.tex Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Fri Jan 18 18:30:19 2002 +0100
@@ -217,7 +217,7 @@
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
\isamarkupfalse%
\isacommand{done}\isamarkupfalse%
%