Performs arithmetic or boolean reduction on a theorem at all levels possible.
LIBRARY
reduce
DESCRIPTION
REDUCE_RULE attempts to transform a theorem by applying REDUCE_CONV.
FAILURE
Never fails, but may just return the original theorem.
EXAMPLE
> reduceLib.REDUCE_RULE (ASSUME “x = 100 + (60 - 17)”);
val it = [.] ⊢ x = 143 : thm
> reduceLib.REDUCE_RULE (REFL “100 + 12 DIV 6”);
val it = ⊢ T : thm