remove_ssfrags : simpset -> string list -> simpset
STRUCTURE
simpLib
SYNOPSIS
Removes named simpset fragments from a simpset.
DESCRIPTION
A call to remove_ssfrags simpset fragnames returns a simpset that is the same as simpset except that the simpset fragments with names in the list fragnames are no longer included.
FAILURE
Never fails. If a name in the list of fragment names does not occur as a name amongst the simpset fragments in the input simpset, no error is reported.
EXAMPLE
- SIMP_CONV (srw_ss()) [] ``MAP ($+ 1) [3;4;5]``;
<<HOL message: Initialising SRW simpset ... done>>
> val it = |- MAP ($+ 1) [3; 4; 5] = [4; 5; 6] : thm

- val myss = simpLib.remove_ssfrags (srw_ss()) ["REDUCE"]
> val myss = ...output elided...

- SIMP_CONV myss [] ``MAP ($+ 1) [3;4;5]``
> val it = |- MAP ($+ 1) [3; 4; 5] = [1 + 3; 1 + 4; 1 + 5] : thm
SEEALSO
diminish_srw_ss
HOL  Kananaskis-14