Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
extend_basic_rewrites : thm list -> unit
SYNOPSIS
Extend the set of default rewrites used by rewriting and simplification.
DESCRIPTION
The HOL Light rewriter (REWRITE_TAC etc.) and simplifier (SIMP_TAC etc.)
have default sets of (conditional) equations and other conversions that are
applied by default, except in the PURE_ variants. A call to
extend_basic_rewrites thl extends the former with the list of theorems thl,
so they will thereafter happen by default.