RW_TAC : simpset -> thm list -> tactic
STRUCTURE
SYNOPSIS
Simplification with case-splitting and built-in knowledge of declared datatypes.
DESCRIPTION
bossLib.RW_TAC is identical to BasicProvers.RW_TAC.
SEEALSO
HOL  Trindemossen-1