Rewrite.add_implicit

Rewrite.add_implicit_rewrites: thm list -> unit

STRUCTURE: Rewrite
SYNOPSIS: Augments the built-in database of simplifications automatically included in rewriting.
USES: Used to build up the power of the built-in simplification set.
SEEALSO: set_implicit_rewrites

HOL Kananaskis-14