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;

added case_conclusion attribute; added coinduct method/attribute; induct method: definsts/fixing/taking; tuned;

improved failure tracking

Datatype_Universe: hide base names only;

added type cases/cases_tactic, and CASES, SUBGOAL_CASES; added consume rule; support named case conclusions; tuned interfaces;

cases_tactic;

moved multi_resolve(s) to drule.ML; cases_tactic;

find_xxxS: term instead of thm;

export map_tags; added multi_resolve(s) -- from Isar/method.ML;

make coinduct actually work; moved some generic code to Pure/Isar/rule_cases.ML; tuned;

Drule.multi_resolves;

declare coinduct rule; tuned;

added code generator syntax

added codegenerator

added code generator syntax

new treatment of polymorphic types, using Sign.const_typargs