# HG changeset patch
# User nipkow
# Date 1153900223 -7200
# Node ID f4a8b4e2fb29bcad611241136db0348f1ba5015f
# Parent  c7f907f41f7c56b979c9fff591f5ddf7f6d71dc2
Removed wrong sentence (Simon Funke)

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