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.

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.