A proper patch that provides z_%mu%_eq_tac is attached. (The implementation is simpler than what I sent before.)


On 16/08/04 13:49, Philip Clayton wrote:
Given a subgoal conclusion (%mu% D | P %spot% V) = x or similar, I've
found that it's helpful to have a tactic that uses z_%mu%_rule to break
the goal into a forall and exists subgoal. This often removes the need
to explicitly mention %mu% TERMs (to apply to z_%mu%_rule) making proofs
more tolerant to changes.

Incase it's useful to anyone (I know Steve King has been fiddling with
%mu%s) I've attached my implementation --- called z_%mu%_eq_tac.

Would there be any value in adding such a tactic to ProofPower?
(Possibly even as a stripping tactic?)


Attachment: patch-2.9.1w2.rda.110226.pbc.110705.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to