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




