REDUCE_RULE : (thm -> thm)
STRUCTURE
reduceLib
SYNOPSIS
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
#REDUCE_RULE (ASSUME "x = (100 + (60 - 17))");;
. |- x = 143

#REDUCE_RULE (REFL "100 + 12 DIV 6");;
|- T
SEEALSO
RED_CONV, REDUCE_CONV, REDUCE_TAC
HOL  Kananaskis-13