doc-src/IsarImplementation/Thy/document/tactic.tex
 changeset 20065 636f84cd3639 parent 20043 036128013178 child 20316 99b6e2900c0f
equal 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
   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.