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

lemma dlist_ext

merged

optionally ignore errors during translation of equations; tuned representation of abstraction points

optionally ignore errors during translation of equations

tolerate eta-variants in f_graph.cases (from inductive package); added test case;