cv_termination_tac : tactic
STRUCTURE
cv_transLib
SYNOPSIS
A tactic for simplifying goals concerning cv_depth_sum.
LIBRARY
cv_transLib
DESCRIPTION
This tactic is used by cv_transLib.cv_trans (and siblings) when attempting to prove termination goals of translated :cv functions.
SEEALSO
cv_trans, cv_trans_pre, cv_trans_pre_rec, cv_trans_rec, cv_auto_trans, cv_auto_trans_pre, cv_auto_trans_pre_rec, cv_auto_trans_rec, cv_eval
HOL  Trindemossen-1