--- 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*}