--- 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%
%