doc-src/IsarImplementation/Thy/Proof.thy
 changeset 46265 b6ab3cdea163 parent 42666 fee67c099d03
equal inserted replaced
46264:f575281fb551 46265:b6ab3cdea163
   385   the parameters in the conclusion, need to exported explicitly into
   385   the parameters in the conclusion, need to exported explicitly into
   386   the original context.  *}
   386   the original context.  *}
   387
   387
   388 text %mlref {*
   388 text %mlref {*
   389   \begin{mldecls}
   389   \begin{mldecls}

   390   @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
   390   @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) ->
   391   @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) ->
   391   Proof.context -> int -> tactic"} \\
   392   Proof.context -> int -> tactic"} \\
   392   @{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) ->
   393   @{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) ->
   393   Proof.context -> int -> tactic"} \\
   394   Proof.context -> int -> tactic"} \\
   394   @{index_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) ->
   395   @{index_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) ->
   410   @{index_ML Obtain.result: "(Proof.context -> tactic) -> thm list ->
   411   @{index_ML Obtain.result: "(Proof.context -> tactic) -> thm list ->
   411   Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\
   412   Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\
   412   \end{mldecls}
   413   \end{mldecls}
   413
   414
   414   \begin{description}
   415   \begin{description}

   416

   417   \item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the

   418   specified subgoal @{text "i"}.  This introduces a nested goal state,

   419   without decomposing the internal structure of the subgoal yet.
   415
   420
   416   \item @{ML SUBPROOF}~@{text "tac ctxt i"} decomposes the structure
   421   \item @{ML SUBPROOF}~@{text "tac ctxt i"} decomposes the structure
   417   of the specified sub-goal, producing an extended context and a
   422   of the specified sub-goal, producing an extended context and a
   418   reduced goal, which needs to be solved by the given tactic.  All
   423   reduced goal, which needs to be solved by the given tactic.  All
   419   schematic parameters of the goal are imported into the context as
   424   schematic parameters of the goal are imported into the context as