WF_REL_TAC : term quotation -> tactic
STRUCTURE
TotalDefn
SYNOPSIS
Initiate a termination proof.
DESCRIPTION
bossLib.WF_REL_TAC
is identical to
TotalDefn.WF_REL_TAC
.
SEEALSO
WF_REL_TAC
HOL
Kananaskis-13