op ++ : simpset * ssfrag -> simpset
STRUCTURE
SYNOPSIS
Infix operator for augmenting simpsets with ssfrag values.
LIBRARY
simpLib
DESCRIPTION
The ++ function combines its two arguments and creates a new simpset. This is a way of creating simpsets that are tailored to the particular simplification task at hand.
FAILURE
Never fails.
EXAMPLE
Here we add the UNWIND_ss ssfrag value to the pure_ss simpset to exploit the former’s point-wise elimination conversions.
- SIMP_CONV (pureSimps.pure_ss ++ boolSimps.UNWIND_ss) []
            (Term`!x. x ==> (?y. P(x,y) /\ (y = 5))`);

> val it = |- (!x. x ==> (?y. P (x,y) /\ (y = 5))) = P (T,5) : thm

SEEALSO
HOL  Kananaskis-13