signature pureSimps = sig val PURE_ss : simpLib.ssfrag val pure_ss : simpLib.simpset end
HOL 4, Trindemossen-1