Item_Net/Named_Thms: export efficient member operation;

initialized atps reference with standard setup in the atp manager

compile

handle SPASS's equality predicate correctly in Isar proof reconstruction

merged

added Isar proof reconstruction support for SPASS -- which means all provers can now yield Isar proofs; the implementation might still be flaky, but exceptions are caught so that a proof reconstruction failure doesn't result in a Sledgehammer failure (the one-line Metis proof might still work after all)

remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed