REDUCE_TAC : tactic
STRUCTURE
reduceLib
SYNOPSIS
Performs arithmetic or boolean reduction on a goal at all levels possible.
LIBRARY
reduce
DESCRIPTION
REDUCE_TAC attempts to transform a goal by applying REDUCE_CONV. It will prove any true goal which is constructed from numerals and the boolean constants T and F.
FAILURE
Never fails, but may not advance the goal.
EXAMPLE
The following example takes a couple of minutes’ CPU time: 

   #g "((1 EXP 3) + (12 EXP 3) = 1729) /\ ((9 EXP 3) + (10 EXP 3) = 1729)";;
   "((1 EXP 3) + (12 EXP 3) = 1729) /\ ((9 EXP 3) + (10 EXP 3) = 1729)"

   () : void

   #e REDUCE_TAC;;
   OK..
   goal proved
   |- ((1 EXP 3) + (12 EXP 3) = 1729) /\ ((9 EXP 3) + (10 EXP 3) = 1729)

   Previous subproof:
   goal proved
   () : void
SEEALSO
RED_CONV, REDUCE_CONV, REDUCE_RULE
HOL  Kananaskis-13