simpLib.mk_simpset : ssfrag list -> simpset
STRUCTURE
simpLib
SYNOPSIS
Creates a simpset by combining a list of
ssfrag
values.
LIBRARY
simpLib
DESCRIPTION
This function creates a
simpset
value by repeatedly adding (as per the
++
operator)
simpset
fragment values to the base
empty_ss
.
FAILURE
Never fails.
USES
Creates simpsets, which are a necessary argument to any simplification function.
SEEALSO
++
,
rewrites
,
SIMP_CONV
HOL
Kananaskis-13