(un)fold: ignore facts;
authorwenzelm
Wed Sep 08 18:10:39 1999 +0200 (1999-09-08)
changeset 75261ea137d3b5bf
parent 7525 2a75abcf30e0
child 7527 9e2dddd8b81f
(un)fold: ignore facts;
doc-src/IsarRef/generic.tex
src/Pure/Isar/method.ML
     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
     2.1 --- a/src/Pure/Isar/method.ML	Wed Sep 08 16:44:11 1999 +0200
     2.2 +++ b/src/Pure/Isar/method.ML	Wed Sep 08 18:10:39 1999 +0200
     2.3 @@ -116,8 +116,8 @@
     2.4  
     2.5  (* fold / unfold definitions *)
     2.6  
     2.7 -val fold = METHOD0 o fold_goals_tac;
     2.8 -val unfold = METHOD0 o rewrite_goals_tac;
     2.9 +fun fold thms = METHOD (fn _ => fold_goals_tac thms);
    2.10 +fun unfold thms = METHOD (fn _ => rewrite_goals_tac thms);
    2.11  
    2.12  
    2.13  (* multi_resolve *)