--- 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}.