# HG changeset patch
# User nipkow
# Date 984591601 -3600
# Node ID 5bea3a8abdc3c1bd96af83977f8959679391b9ab
# Parent  67cec35dbc58984388774751c0696ebf24bf9eb5
*** empty log message ***

diff -r 67cec35dbc58 -r 5bea3a8abdc3 doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Wed Mar 14 17:38:49 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Wed Mar 14 18:40:01 2001 +0100
@@ -123,7 +123,17 @@
 Both \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} and \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} run forever on
 the problematic subgoal above.
 Note that only one of the modifiers is allowed, and it must precede all
-other arguments.%
+other arguments.
+
+\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}rotate{\isacharunderscore}tac}~$n$\isa{{\isacharparenright}}\indexbold{*rotate_tac}
+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}%
 %
 \isamarkupsubsubsection{Rewriting with Definitions%
diff -r 67cec35dbc58 -r 5bea3a8abdc3 doc-src/TutorialI/Misc/simp.thy
--- a/doc-src/TutorialI/Misc/simp.thy	Wed Mar 14 17:38:49 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy	Wed Mar 14 18:40:01 2001 +0100
@@ -121,6 +121,16 @@
 the problematic subgoal above.
 Note that only one of the modifiers is allowed, and it must precede all
 other arguments.
+
+\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"(rotate_tac"}~$n$@{text")"}\indexbold{*rotate_tac}
+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}
 *}
 
 subsubsection{*Rewriting with Definitions*}
diff -r 67cec35dbc58 -r 5bea3a8abdc3 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Wed Mar 14 17:38:49 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Wed Mar 14 18:40:01 2001 +0100
@@ -57,8 +57,6 @@
 
 Advanced recdef: explain recdef_tc?
 
-warning: simp of asms from l to r; may require reordering (rotate_tac)
-
 Adjust FP textbook refs: new Bird, Hudak
 Discrete math textbook: Rosen?