set_implicit_rewrites: rewrites -> unit
STRUCTURE
SYNOPSIS
Allows the user to control the built-in database of simplifications used in rewriting.
FAILURE
Never fails.
SEEALSO
HOL  Kananaskis-13