--- a/doc-src/TutorialI/CTL/CTL.thy Wed Aug 04 09:44:40 2004 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy Wed Aug 04 11:25:08 2004 +0200
@@ -125,7 +125,9 @@
txt{*
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
In this remaining case, we set @{term t} to @{term"p(1::nat)"}.
-The rest is automatic.
+The rest is automatic, which is surprising because it involves
+finding the instantiation @{term"\<lambda>i::nat. p(i+1)"}
+for @{text"\<forall>p"}.
*};
apply(erule_tac x = "p 1" in allE);
--- a/doc-src/TutorialI/CTL/document/CTL.tex Wed Aug 04 09:44:40 2004 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed Aug 04 11:25:08 2004 +0200
@@ -126,7 +126,9 @@
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
\end{isabelle}
In this remaining case, we set \isa{t} to \isa{p\ {\isadigit{1}}}.
-The rest is automatic.%
+The rest is automatic, which is surprising because it involves
+finding the instantiation \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}
+for \isa{{\isasymforall}p}.%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline