doc-src/IsarImplementation/Thy/document/Proof.tex
changeset 46265 b6ab3cdea163
parent 42666 fee67c099d03
child 46525 af3df09590f9
equal deleted inserted replaced
46264:f575281fb551 46265:b6ab3cdea163
   586 %
   586 %
   587 \isatagmlref
   587 \isatagmlref
   588 %
   588 %
   589 \begin{isamarkuptext}%
   589 \begin{isamarkuptext}%
   590 \begin{mldecls}
   590 \begin{mldecls}
       
   591   \indexdef{}{ML}{SELECT\_GOAL}\verb|SELECT_GOAL: tactic -> int -> tactic| \\
   591   \indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: (Subgoal.focus -> tactic) ->|\isasep\isanewline%
   592   \indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: (Subgoal.focus -> tactic) ->|\isasep\isanewline%
   592 \verb|  Proof.context -> int -> tactic| \\
   593 \verb|  Proof.context -> int -> tactic| \\
   593   \indexdef{}{ML}{Subgoal.FOCUS}\verb|Subgoal.FOCUS: (Subgoal.focus -> tactic) ->|\isasep\isanewline%
   594   \indexdef{}{ML}{Subgoal.FOCUS}\verb|Subgoal.FOCUS: (Subgoal.focus -> tactic) ->|\isasep\isanewline%
   594 \verb|  Proof.context -> int -> tactic| \\
   595 \verb|  Proof.context -> int -> tactic| \\
   595   \indexdef{}{ML}{Subgoal.FOCUS\_PREMS}\verb|Subgoal.FOCUS_PREMS: (Subgoal.focus -> tactic) ->|\isasep\isanewline%
   596   \indexdef{}{ML}{Subgoal.FOCUS\_PREMS}\verb|Subgoal.FOCUS_PREMS: (Subgoal.focus -> tactic) ->|\isasep\isanewline%
   612 \verb|  Proof.context -> ((string * cterm) list * thm list) * Proof.context| \\
   613 \verb|  Proof.context -> ((string * cterm) list * thm list) * Proof.context| \\
   613   \end{mldecls}
   614   \end{mldecls}
   614 
   615 
   615   \begin{description}
   616   \begin{description}
   616 
   617 
       
   618   \item \verb|SELECT_GOAL|~\isa{tac\ i} confines a tactic to the
       
   619   specified subgoal \isa{i}.  This introduces a nested goal state,
       
   620   without decomposing the internal structure of the subgoal yet.
       
   621 
   617   \item \verb|SUBPROOF|~\isa{tac\ ctxt\ i} decomposes the structure
   622   \item \verb|SUBPROOF|~\isa{tac\ ctxt\ i} decomposes the structure
   618   of the specified sub-goal, producing an extended context and a
   623   of the specified sub-goal, producing an extended context and a
   619   reduced goal, which needs to be solved by the given tactic.  All
   624   reduced goal, which needs to be solved by the given tactic.  All
   620   schematic parameters of the goal are imported into the context as
   625   schematic parameters of the goal are imported into the context as
   621   fixed ones, which may not be instantiated in the sub-proof.
   626   fixed ones, which may not be instantiated in the sub-proof.