signature rich_listSimps = sig val add_rich_list_compset : computeLib.compset -> unit val RICH_LIST_ss : simpLib.ssfrag end
HOL 4, Kananaskis-14