Re: [isabelle] Normalizing Pure.conjunction/Pure.all
> You did not say how you got there. Note that
> Goal.recover_conjunction_tac happens to be available for this, because
> it is occasionally needed in obscure situations.
This particular goal state arises in a tool. In a nutshell, I start with
"Goal.prove_common" and supply multiple propositions (let's say "P" and
"Q"). Then, I need to preprocess these propositions (let's say some
extensionality rule) so that I can apply induction. Hence, I need to
- break off the Pure conjunction ("conjunction_tac"),
- apply the preprocessing ("ALLGOALS"),
- recover the conjunction ("recover_conjunction_tac"),
- move out the quantifiers, and
- perform induction.
This archive was generated by a fusion of
Pipermail (Mailman edition) and