# HG changeset patch
# User nipkow
# Date 1033631694 -7200
# Node ID c2b235e60f8bf76c78f08217f165bd6d50bbd871
# Parent  9768ba6ab5e79aaf30764b90735fc6cd4ae2bf1f
*** empty log message ***

diff -r 9768ba6ab5e7 -r c2b235e60f8b doc-src/TutorialI/CTL/document/CTLind.tex
--- 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}%
diff -r 9768ba6ab5e7 -r c2b235e60f8b doc-src/TutorialI/Misc/document/simp.tex
--- 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%
 %
diff -r 9768ba6ab5e7 -r c2b235e60f8b doc-src/TutorialI/Misc/simp.thy
--- 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*}