doc-src/IsarImplementation/Thy/Proof.thy
changeset 46265 b6ab3cdea163
parent 42666 fee67c099d03
equal deleted 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