# HG changeset patch # User nipkow # Date 1091611508 -7200 # Node ID e8cef6993701a74d3c1ac04f56fd5b6b597ed3df # Parent e194d4d265fb72722b0de061d43fc6c53f15cc2a aded comment diff -r e194d4d265fb -r e8cef6993701 doc-src/TutorialI/CTL/CTL.thy --- 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"\i::nat. p(i+1)"} +for @{text"\p"}. *}; apply(erule_tac x = "p 1" in allE); diff -r e194d4d265fb -r e8cef6993701 doc-src/TutorialI/CTL/document/CTL.tex --- 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