REDUCE_RULE : (thm -> thm)

- STRUCTURE
- 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

HOL Kananaskis-14