signature extrealSimps = sig (* Extended real inequality simps to generally be used with augment_srw_ss *) val EXTREAL_ss : simpLib.ssfrag; end
HOL 4, Trindemossen-1