doc-src/TutorialI/Misc/document/simp.tex
changeset 20212 f4a8b4e2fb29
parent 20144 2517cd4b1f37
child 27027 63f0b638355c
--- 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}