signature rich_listSimps = sig val add_rich_list_compset : computeLib.compset -> computeLib.compset val RICH_LIST_ss : simpLib.ssfrag end
HOL 4, Trindemossen-2