[ProofPower] DEPTH_CONV

[Stephen Brackin]

HOL90 has a conversion (conversional?) called DEPTH_CONV that, when applied
to a conversion CV, produces a new conversion that applies CV to every
subterm of its argument.

CONV_TAC (DEPTH_CONV CV) applies CV to every subterm of the goal.

How do I get the same effect in ProofPower?  It doesn't seem to happen
automatically.

Steve

Stephen Brackin
Senior Security Analyst
CygnaCom Solutions, Inc.
an Entrust company
Phone: 607-277-8211 Fax:  607-277-8211
http://www.cygnacom.com

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040916/461326a5/attachment.htm>