# HG changeset patch
# User nipkow
# Date 1008677721 -3600
# Node ID e417bd7ca8a0348e4bf30dac3433fb7568330e25
# Parent  7e51804da8f4f576b5472ccbb5b16ebef24db499
*** empty log message ***

diff -r 7e51804da8f4 -r e417bd7ca8a0 doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Tue Dec 18 02:22:27 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Tue Dec 18 13:15:21 2001 +0100
@@ -237,7 +237,8 @@
 There is also the special method \isa{unfold}\index{*unfold (method)|bold}
 which merely unfolds
 one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}.
-This is can be useful in situations where \isa{simp} does too much.%
+This is can be useful in situations where \isa{simp} does too much.
+Warning: \isa{unfold} acts on all subgoals!%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 7e51804da8f4 -r e417bd7ca8a0 doc-src/TutorialI/Misc/simp.thy
--- a/doc-src/TutorialI/Misc/simp.thy	Tue Dec 18 02:22:27 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy	Tue Dec 18 13:15:21 2001 +0100
@@ -202,6 +202,7 @@
 which merely unfolds
 one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}.
 This is can be useful in situations where \isa{simp} does too much.
+Warning: \isa{unfold} acts on all subgoals!
 *}
 
 subsection{*Simplifying {\tt\slshape let}-Expressions*}