--- a/doc-src/IsarRef/generic.tex Wed Sep 08 16:44:11 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Wed Sep 08 18:10:39 1999 +0200
@@ -46,7 +46,8 @@
$rule$ (single step, involving facts) or $elim$ (multiple steps, see
\S\ref{sec:classical-basic}).
\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
- meta-level definitions throughout all goals; facts may not be involved.
+ meta-level definitions throughout all goals; any facts provided are
+ \emph{ignored}.
\item [$succeed$] yields a single (unchanged) result; it is the identify of
the ``\texttt{,}'' method combinator.
\item [$fail$] yields an empty result sequence; it is the identify of the