signature sumSimps = sig val SUM_ss : simpLib.ssfrag val SUM_rws : computeLib.compset -> computeLib.compset end
HOL 4, Trindemossen-2