doc-src/IsarImplementation/Thy/document/tactic.tex
changeset 20065 636f84cd3639
parent 20043 036128013178
child 20316 99b6e2900c0f
equal deleted inserted replaced
20064:92aad017b847 20065:636f84cd3639
   211   presented as facts.  The result is essentially \isa{{\isasymAnd}xs{\isachardot}\ As\ {\isasymLongrightarrow}\ C}, but is normalized by pulling \isa{{\isasymAnd}} before \isa{{\isasymLongrightarrow}}
   211   presented as facts.  The result is essentially \isa{{\isasymAnd}xs{\isachardot}\ As\ {\isasymLongrightarrow}\ C}, but is normalized by pulling \isa{{\isasymAnd}} before \isa{{\isasymLongrightarrow}}
   212   (the conclusion \isa{C} itself may be a rule statement), turning
   212   (the conclusion \isa{C} itself may be a rule statement), turning
   213   the quantifier prefix into schematic variables, and generalizing
   213   the quantifier prefix into schematic variables, and generalizing
   214   implicit type-variables.
   214   implicit type-variables.
   215 
   215 
   216   Any additional fixed variables or hypotheses not being mentioned in
       
   217   the initial statement are left unchanged --- programmed proofs may
       
   218   well occur in a larger context.
       
   219 
       
   220   \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
   216   \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
   221   states several conclusions simultaneously.  \verb|Tactic.conjunction_tac| may be used to split these into individual
   217   states several conclusions simultaneously.  \verb|Tactic.conjunction_tac| may be used to split these into individual
   222   subgoals before commencing the actual proof.
   218   subgoals before commencing the actual proof.
   223 
   219 
   224   \item \verb|Goal.prove_global| is a degraded version of \verb|Goal.prove| for theory level goals; it includes a global \verb|Drule.standard| for the result.
   220   \item \verb|Goal.prove_global| is a degraded version of \verb|Goal.prove| for theory level goals; it includes a global \verb|Drule.standard| for the result.