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