set_basic_convs : (string * (term * conv)) list -> unit
- SYNOPSIS
-
Assign the set of default conversions.
- 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. The latter are normally
term transformations that cannot be expressed as single (conditional or
unconditional) rewrite rules. A call to set_basic_convs l where l is a list
of items ("name",(`pat`,conv)) will make the default conversions just that set,
using the name name to refer to each one and restricting it to subterms
encountered that match pat.
- FAILURE CONDITIONS
-
Never fails.
- COMMENTS
-
Normally, users will only want to extend the existing set of conversions using
extend_basic_convs.
- SEE ALSO
-
basic_convs, extend_basic_convs, set_basic_rewrites, REWRITE_TAC, SIMP_TAC.