doc-src/TutorialI/Misc/simp.thy
changeset 12473 f41e477576b9
parent 12332 aea72a834c85
child 12489 c92e38c3cbaa
--- a/doc-src/TutorialI/Misc/simp.thy	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy	Wed Dec 12 09:04:20 2001 +0100
@@ -197,6 +197,11 @@
   $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}
+
+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.
 *}
 
 subsection{*Simplifying {\tt\slshape let}-Expressions*}