aded comment
authornipkow
Wed Aug 04 11:25:08 2004 +0200 (2004-08-04)
changeset 15106e8cef6993701
parent 15105 e194d4d265fb
child 15107 f233706d9fce
aded comment
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/document/CTL.tex
     1.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Wed Aug 04 09:44:40 2004 +0200
     1.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Wed Aug 04 11:25:08 2004 +0200
     1.3 @@ -125,7 +125,9 @@
     1.4  txt{*
     1.5  @{subgoals[display,indent=0,margin=70,goals_limit=1]}
     1.6  In this remaining case, we set @{term t} to @{term"p(1::nat)"}.
     1.7 -The rest is automatic.
     1.8 +The rest is automatic, which is surprising because it involves
     1.9 +finding the instantiation @{term"\<lambda>i::nat. p(i+1)"}
    1.10 +for @{text"\<forall>p"}.
    1.11  *};
    1.12  
    1.13  apply(erule_tac x = "p 1" in allE);
     2.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Wed Aug 04 09:44:40 2004 +0200
     2.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Wed Aug 04 11:25:08 2004 +0200
     2.3 @@ -126,7 +126,9 @@
     2.4  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
     2.5  \end{isabelle}
     2.6  In this remaining case, we set \isa{t} to \isa{p\ {\isadigit{1}}}.
     2.7 -The rest is automatic.%
     2.8 +The rest is automatic, which is surprising because it involves
     2.9 +finding the instantiation \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}
    2.10 +for \isa{{\isasymforall}p}.%
    2.11  \end{isamarkuptxt}%
    2.12  \isamarkuptrue%
    2.13  \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline