--- a/doc-src/IsarImplementation/Thy/document/tactic.tex Sat Jul 08 14:01:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/tactic.tex Sat Jul 08 14:12:13 2006 +0200
@@ -213,10 +213,6 @@
the quantifier prefix into schematic variables, and generalizing
implicit type-variables.
- Any additional fixed variables or hypotheses not being mentioned in
- the initial statement are left unchanged --- programmed proofs may
- well occur in a larger context.
-
\item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
states several conclusions simultaneously. \verb|Tactic.conjunction_tac| may be used to split these into individual
subgoals before commencing the actual proof.
--- a/doc-src/IsarImplementation/Thy/tactic.thy Sat Jul 08 14:01:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/tactic.thy Sat Jul 08 14:12:13 2006 +0200
@@ -174,10 +174,6 @@
the quantifier prefix into schematic variables, and generalizing
implicit type-variables.
- Any additional fixed variables or hypotheses not being mentioned in
- the initial statement are left unchanged --- programmed proofs may
- well occur in a larger context.
-
\item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
states several conclusions simultaneously. @{ML
Tactic.conjunction_tac} may be used to split these into individual