# HG changeset patch
# User wenzelm
# Date 936720580 -7200
# Node ID 212516006d89e75195fd67f038bbe33eae6bda29
# Parent  d6fc3c4423f7d5a87e83590a9646a6285660eb8a
tuned (then_)apply;

diff -r d6fc3c4423f7 -r 212516006d89 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Sep 07 18:09:18 1999 +0200
+++ b/doc-src/IsarRef/pure.tex	Tue Sep 07 18:09:40 1999 +0200
@@ -714,9 +714,9 @@
 
 \begin{descr}
 \item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in the
-  plain-old-tactic sense.  Facts for forward chaining are ignored.
+  plain-old-tactic sense.  Facts for forward chaining are reset.
 \item [$\isarkeyword{then_apply}~(m)$] is similar to $\isarkeyword{apply}$,
-  but observes the goal's facts.
+  but keeps the goal's facts.
 \item [$\isarkeyword{back}$] does back-tracking over the result sequence of
   the latest proof command.\footnote{Unlike the ML function \texttt{back}
     \cite{isabelle-ref}, the Isar command does not search upwards for further