renaming mk_prems to flatten in the function flattening

simplifying function flattening

removed warning_count (known causes for warnings have been resolved)

remove the iteration counter from Sledgehammer's minimizer

merged

start work on direct proof reconstruction for Sledgehammer

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

handle hidden polymorphism in class target (without class target syntax, though)

replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;

replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;

add_axiom: axiomatize "unconstrained" version, with explicit of_class premises; more uniform add_axiom/add_def;

Logic.mk_of_sort convenience;

more explicit invented name;

minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';

do not open ML structures;

modernized overloaded definitions;

standard headers;

slightly more uniform definitions -- eliminated old-style meta-equality;

eliminated old constdefs;

corrected setup for of_list

renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;