--- a/doc-src/IsarImplementation/Thy/Proof.thy Mon Feb 16 21:23:34 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Mon Feb 16 21:39:19 2009 +0100
@@ -302,11 +302,11 @@
\begin{description}
- \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a
- particular sub-goal, producing an extended context and a reduced
- goal, which needs to be solved by the given tactic. All schematic
- parameters of the goal are imported into the context as fixed ones,
- which may not be instantiated in the sub-proof.
+ \item @{ML SUBPROOF}~@{text "tac ctxt i"} decomposes the structure
+ of the specified sub-goal, producing an extended context and a
+ reduced goal, which needs to be solved by the given tactic. All
+ schematic parameters of the goal are imported into the context as
+ fixed ones, which may not be instantiated in the sub-proof.
\item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
"C"} in the context augmented by fixed variables @{text "xs"} and