[ProofPower] DEPTH_CONV

[Roger Bishop Jones]

On Thursday 16 September 2004  9:00 am, Stephen Brackin wrote:
> 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.

Probably one of MAP_C, ONCE_MAP_C, TOP_MAP_C, I don't know
which if any corresponds exactly to DEPTH_CONV, most likely
MAP_C.

Conversionals all end in _C so if you look in the reference
manual KWIC index for C you see all the available conversionals
grouped together.

Roger Jones