equal
deleted
inserted
replaced
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 |