--- a/doc-src/TutorialI/CTL/document/CTLind.tex Wed Oct 02 17:25:31 2002 +0200
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex Thu Oct 03 09:54:54 2002 +0200
@@ -110,9 +110,10 @@
\begin{isamarkuptxt}%
\noindent
\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\isanewline
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ {\isasymforall}y{\isachardot}\ }y\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isasymrbrakk}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ {\isasymforall}y{\isachardot}\ }y\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ }t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ }{\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\isanewline
\isaindent{\ {\isadigit{2}}{\isachardot}\ }wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
--- a/doc-src/TutorialI/Misc/document/simp.tex Wed Oct 02 17:25:31 2002 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex Thu Oct 03 09:54:54 2002 +0200
@@ -159,16 +159,15 @@
the problematic subgoal above.
Only one of the modifiers is allowed, and it must precede all
other modifiers.
-
-\begin{warn}
-Assumptions are simplified in a left-to-right fashion. If an
-assumption can help in simplifying one to the left of it, this may get
-overlooked. In such cases you have to rotate the assumptions explicitly:
-\isacommand{apply}\isa{{\isacharparenleft}}\methdx{rotate_tac}~$n$\isa{{\isacharparenright}}
-causes a cyclic shift by $n$ positions from right to left, if $n$ is
-positive, and from left to right, if $n$ is negative.
-Beware that such rotations make proofs quite brittle.
-\end{warn}%
+%\begin{warn}
+%Assumptions are simplified in a left-to-right fashion. If an
+%assumption can help in simplifying one to the left of it, this may get
+%overlooked. In such cases you have to rotate the assumptions explicitly:
+%\isacommand{apply}@ {text"("}\methdx{rotate_tac}~$n$@ {text")"}
+%causes a cyclic shift by $n$ positions from right to left, if $n$ is
+%positive, and from left to right, if $n$ is negative.
+%Beware that such rotations make proofs quite brittle.
+%\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/TutorialI/Misc/simp.thy Wed Oct 02 17:25:31 2002 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy Thu Oct 03 09:54:54 2002 +0200
@@ -138,16 +138,15 @@
the problematic subgoal above.
Only one of the modifiers is allowed, and it must precede all
other modifiers.
-
-\begin{warn}
-Assumptions are simplified in a left-to-right fashion. If an
-assumption can help in simplifying one to the left of it, this may get
-overlooked. In such cases you have to rotate the assumptions explicitly:
-\isacommand{apply}@{text"("}\methdx{rotate_tac}~$n$@{text")"}
-causes a cyclic shift by $n$ positions from right to left, if $n$ is
-positive, and from left to right, if $n$ is negative.
-Beware that such rotations make proofs quite brittle.
-\end{warn}
+%\begin{warn}
+%Assumptions are simplified in a left-to-right fashion. If an
+%assumption can help in simplifying one to the left of it, this may get
+%overlooked. In such cases you have to rotate the assumptions explicitly:
+%\isacommand{apply}@ {text"("}\methdx{rotate_tac}~$n$@ {text")"}
+%causes a cyclic shift by $n$ positions from right to left, if $n$ is
+%positive, and from left to right, if $n$ is negative.
+%Beware that such rotations make proofs quite brittle.
+%\end{warn}
*}
subsection{*Rewriting with Definitions*}