--- a/doc-src/TutorialI/Rules/rules.tex Sat Mar 21 12:37:13 2009 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Sun Mar 22 19:36:04 2009 +0100
@@ -2138,11 +2138,11 @@
\index{*insert (method)|(}%
The \isa{insert} method
-inserts a given theorem as a new assumption of the current subgoal. This
+inserts a given theorem as a new assumption of all subgoals. This
already is a forward step; moreover, we may (as always when using a
theorem) apply
\isa{of}, \isa{THEN} and other directives. The new assumption can then
-be used to help prove the subgoal.
+be used to help prove the subgoals.
For example, consider this theorem about the divides relation. The first
proof step inserts the distributive law for