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
patch-2.9.1w2.rda.110226.pbc.110705.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
