signature sumSimps = sig val SUM_ss : simpLib.ssfrag val SUM_rws : computeLib.compset -> unit end
HOL 4, Kananaskis-13