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