# HG changeset patch
# User wenzelm
# Date 955576341 -7200
# Node ID 37cbb053791cc405acebc0558737357b327ae371
# Parent  850e845267454c5016362a7f2d2ee9ebf5e2c89e
tuned;

diff -r 850e84526745 -r 37cbb053791c doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Wed Apr 12 23:51:57 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Wed Apr 12 23:52:21 2000 +0200
@@ -1028,8 +1028,8 @@
   indicates any current facts for forward-chaining, and
   \texttt{thm}~/~\texttt{thms} retrieve named facts (including global
   theorems) from the context.
-\item [$insert~\vec a$] inserts theorems as facts into the proof state; the
-  current facts indicated for forward chaining are ignored!
+\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
+  state; the current facts indicated for forward chaining are ignored!
 \item [$res_inst_tac$ etc.] do resolution of rules with explicit
   instantiation.  This works the same way as the corresponding ML tactics, see
   \cite[\S3]{isabelle-ref}.