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