diff -r c7f907f41f7c -r f4a8b4e2fb29 doc-src/TutorialI/Misc/simp.thy
--- a/doc-src/TutorialI/Misc/simp.thy	Wed Jul 26 00:44:49 2006 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy	Wed Jul 26 09:50:23 2006 +0200
@@ -134,8 +134,6 @@
  means that the assumptions are simplified but are not
   used in the simplification of each other or the conclusion.
 \end{description}
-Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on
-the problematic subgoal above.
 Only one of the modifiers is allowed, and it must precede all
 other modifiers.
 %\begin{warn}