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