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

minor code cleanup

if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing

"remote_e" and "remote_vampire" support TSTP proof output + fix "overlord" mode ATP output postprocessing

Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes; this solves the unification exception that consistently was thrown for Cezary's "FSet3" theory

postprocess ATP output in "overlord" mode to make it more readable

failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is

generate command-line in addition to timestamp in ATP output file, for debugging purposes

pass relevant options from "sledgehammer" to "sledgehammer minimize"; one nice side effect of this change is that the "sledgehammer minimize" syntax now only occurs in "sledgehammer_isar.ML", instead of being spread across two files

Finite set theory

merged

Tidied up using s/l

split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;

fun_rel introduction and list_rel elimination for quotient package

lemmas concerning remdups