QUANT_CONV : conv -> conv
STRUCTURE
SYNOPSIS
Applies a conversion underneath a quantifier.
DESCRIPTION
If conv N returns A |- N = P, then QUANT_CONV conv (M (\v.N)) returns A |- M (\v.N) = M (\v.P).
FAILURE
If conv N fails, or if v is free in A.
EXAMPLE
- QUANT_CONV SYM_CONV (Term `!x. x + 0 = x`);
> val it = |- (!x. x + 0 = x) = !x. x = x + 0 : thm
COMMENTS
For deeply nested quantifiers, STRIP_QUANT_CONV and STRIP_BINDER_CONV are more efficient than iterated application of QUANT_CONV, BINDER_CONV, or ABS_CONV.
SEEALSO
HOL  Kananaskis-14