signature indexedListsSimps = sig val add_indexedLists_compset : computeLib.compset -> unit val indexedLists_ss : simpLib.ssfrag end
HOL 4, Trindemossen-1