# HG changeset patch
# User wenzelm
# Date 1152360733 7200
# Node ID 636f84cd363924dfceaf3c563e7ffb79ca982e6c
# Parent 92aad017b847cbe3447b5b44009a6ad9a11c1266
tuned;
diff r 92aad017b847 r 636f84cd3639 docsrc/IsarImplementation/Thy/document/tactic.tex
 a/docsrc/IsarImplementation/Thy/document/tactic.tex Sat Jul 08 14:01:40 2006 +0200
+++ b/docsrc/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 typevariables.
 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 \verbGoal.prove_multi is simular to \verbGoal.prove, but
states several conclusions simultaneously. \verbTactic.conjunction_tac may be used to split these into individual
subgoals before commencing the actual proof.
diff r 92aad017b847 r 636f84cd3639 docsrc/IsarImplementation/Thy/tactic.thy
 a/docsrc/IsarImplementation/Thy/tactic.thy Sat Jul 08 14:01:40 2006 +0200
+++ b/docsrc/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 typevariables.
 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