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