doc-src/IsarImplementation/Thy/tactic.thy
changeset 20065 636f84cd3639
parent 20042 2308529f8e8d
child 20316 99b6e2900c0f
equal deleted inserted replaced
20064:92aad017b847 20065:636f84cd3639
   172   C"}, but is normalized by pulling @{text "\<And>"} before @{text "\<Longrightarrow>"}
   172   C"}, but is normalized by pulling @{text "\<And>"} before @{text "\<Longrightarrow>"}
   173   (the conclusion @{text "C"} itself may be a rule statement), turning
   173   (the conclusion @{text "C"} itself may be a rule statement), turning
   174   the quantifier prefix into schematic variables, and generalizing
   174   the quantifier prefix into schematic variables, and generalizing
   175   implicit type-variables.
   175   implicit type-variables.
   176 
   176 
   177   Any additional fixed variables or hypotheses not being mentioned in
       
   178   the initial statement are left unchanged --- programmed proofs may
       
   179   well occur in a larger context.
       
   180 
       
   181   \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
   177   \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
   182   states several conclusions simultaneously.  @{ML
   178   states several conclusions simultaneously.  @{ML
   183   Tactic.conjunction_tac} may be used to split these into individual
   179   Tactic.conjunction_tac} may be used to split these into individual
   184   subgoals before commencing the actual proof.
   180   subgoals before commencing the actual proof.
   185 
   181