DECIDE_TAC : tactic
STRUCTURE
bossLib
SYNOPSIS
Invoke decision procedure(s).
DESCRIPTION
DECIDE_TAC
is the tactical version of
DECIDE
.
FAILURE
As for
DECIDE
SEEALSO
DECIDE
HOL
Trindemossen-1