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

set "atps" reference's default value to "(remote_)e (remote_)spass (remote_)vampire", based on what is installed