signature SatisfySimps = sig val SATISFY_REDUCER : Traverse.reducer; val SATISFY_ss : simpLib.ssfrag end;
HOL 4, Kananaskis-10