RW_TAC

BasicProvers.RW_TAC : simpset -> thm list -> tactic

Simplification with case-splitting and built-in knowledge of declared datatypes.

bossLib.RW_TAC is identical to BasicProvers.RW_TAC.

See also

bossLib.RW_TAC