Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. Still have old verions of "vampireH","vampireF", "eproverH", "eproverF", which can be called to handle HOL or FOL problems.

Only output arities and class relations if !ResClause.keep_types is true.

some small tuning

ISAR-fied two proofs about equality for abstraction functions.

* Provers/induct: obtain pattern;

added an authors section (please let me know if somebody is left out or unhappy)

some minor tunings

added the version of nominal.thy that contains all properties about support of finite sets

cleaned up all examples so that they work with the current nominal-setting.

finished cleaning up the parts that collect lemmas (with instantiations) under some general names

Corrected treatment of non-recursive abstraction types.

tuned induct proofs;

induct: insert defs in object-logic form; export guess_instance;

tuned induct proofs;

tuned induct proofs;

consume: unfold defs in all major prems;

revert_skolem: fall back on Syntax.deskolem;

forall_conv ~1;

added dummy_pattern;

tuned names;

forall_conv: limit prefix;

fix_tac: proper treatment of major premises in goal; export atomize/rulify interface; tuned;

removed obsolete dummy paragraphs;

tuned;

code generator: case expressions, improved name resolving

added fsub.thy (poplmark challenge) to the examples directory.

Fixed problem with strong induction theorem for datatypes containing no atom types (ind_sort was the empty sort in this case).

send more information with test-takes-too-long message (which tests are still running)

fixed spelling of 'case_conclusion';

tuned induct proofs;