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

Phil


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?)

Phil

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

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to