doc-src/IsarImplementation/Thy/document/Proof.tex
 changeset 46265 b6ab3cdea163 parent 42666 fee67c099d03 child 46525 af3df09590f9
equal 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.