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