# HG changeset patch
# User wenzelm
# Date 1152360733 -7200
# Node ID 636f84cd363924dfceaf3c563e7ffb79ca982e6c
# Parent  92aad017b847cbe3447b5b44009a6ad9a11c1266
tuned;

diff -r 92aad017b847 -r 636f84cd3639 doc-src/IsarImplementation/Thy/document/tactic.tex
--- 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.
diff -r 92aad017b847 -r 636f84cd3639 doc-src/IsarImplementation/Thy/tactic.thy
--- 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