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;