doc-src/TutorialI/Misc/document/simp.tex

 \begin{warn}
   If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
   occurrences of $f$ with at least two arguments. This may be helpful for unfolding
   $f$ selectively, but it may also get in the way. Defining
   $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
-\end{warn}%
+\end{warn}
+
+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 if \isa{simp} does too much.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Simplifying {\tt\slshape let}-Expressions%
 }