diff -r c7f907f41f7c -r f4a8b4e2fb29 doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Wed Jul 26 00:44:49 2006 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Wed Jul 26 09:50:23 2006 +0200
@@ -193,8 +193,6 @@
  means that the assumptions are simplified but are not
   used in the simplification of each other or the conclusion.
 \end{description}
-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.
 Only one of the modifiers is allowed, and it must precede all
 other modifiers.
 %\begin{warn}