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;

tuned induction proofs;

more robust revert_skolem; tuned;

tuned;

Provers/induct: definitional insts and fixing;

consume: proper treatment of defs; simplified case_conclusion;

added case_conclusion attribute;

(co)induct: taking; induct set: proper treatment of defs;

RuleCases.case_conclusion;

tuned;