renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
"full" sounds like "full types" or something, not like a structured Isar proof -- at some point I hope to make this an option that's orthogonal to the prover

move all ATP setup code into ATP_Wrapper

move the Sledgehammer Isar commands together into one file;
this will make easier to add options and reorganize them later

more Sledgehammer refactoring

use a proof context instead of a local theory

provide a hook to safely manipulate verification conditions

replaced old-style Drule.add_axiom by Specification.axiomatization

removed e-mail address from error message

merged

tuned whitespace