FULL_SIMP_TAC : simpset -> thm list -> tactic
STRUCTURE
simpLib
SYNOPSIS
Simplify a term with the given simpset and theorems.
DESCRIPTION
bossLib.FULL_SIMP_TAC
is identical to
simpLib.FULL_SIMP_TAC
.
SEEALSO
FULL_SIMP_TAC
HOL
Trindemossen-1