minor improvements

modified almost everything for the new nominal_induct (at the end there are some "normal" inductions which need a bit more attention)

Changed order of predicate arguments and quantifiers in strong induction rule.

fixed the lemma where the new names generated by nominal_induct caused problems.

added one clause for substitution in the lambda-case and mad it globally [simp]

added rename_params_rule: recover orginal fresh names in subgoals/cases;

changed induction principle and everything to conform with the new nominal_induct

fresh: frees instead of terms, rename corresponding params in rule; tuned;

adapted to the new nominal_induction

changed \<sim> of permutation equality to \<triangleq> (Jesper wanted to use \<sim>).

fresh_unit_elim and fresh_prod_elim -- for nominal_induct;

reimplement Case expression pattern matching to support lazy patterns

add definitions as defs, not axioms

changed section names

add xsymbol syntax for u type constructor

add constant unit_when

proper treatment of tuple/tuple_fun -- nest to the left!

moved nth_list to Pure/library.ML;

added nth_list;

added mk_split;

changed the order of the induction variable and the context in lam_induct (test to see whether it simplifies the code for nominal_induct).

reworked version with proper support for defs, fixes, fresh specification;

added haskell serializer

exported customized syntax interface

Corrected atom class constraints in strong induction rule.

made some of the theorem look-ups static (by using thm instead of PureThy.get_thm)

added (curried) fold2

added proof of measure_induct_rule;

Added flags for setting and detecting whether a problem needs combinators.

Only output types if !keep_types is true.

Added two functions for CNF translation, used by other files.

Added in four control flags for HOL and FOL translations. Changed functions that perform HOL/FOL translations, and write ATP input to files. Removed some functions that are no longer needed.

Slight modification to trace information.

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;