| changeset 12533 | e417bd7ca8a0 |
| parent 12489 | c92e38c3cbaa |
| child 12582 | b85acd66f715 |
--- 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*}