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