step towards proper purge operation

put declarations first

clarified terminology

intermediate cleanup

clarified relationship of code generator conversions and evaluations

abs_conv/forall_conv: proper context (avoid gensym); removed unused cache_conv;

load variable.ML before conv.ML;

Conv.forall_conv: proper context;

cover AFP logs as well, using "afp" pseudo-platform;

moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;

avoid gensym;

updated Sign.add_abbrev;

combinator translation

avoid unnamed infixes;

avoid unnamed infixes; tuned;

avoid unnamed infixes;

modernized specifications; tuned proofs;

mark inductive results as internal;

skolem_cache: ignore internal theorems -- major speedup; skolem_cache_theorems_of: efficient folding of table; replaced get_axiom by Thm.get_axiom_i (avoids name space fishing);

major speedup by avoiding metis;

modernized definitions;

added add_defs_new, which strips sorts for axioms (presently inactive);

removed unused add_defss;

tuned internal inductive interface;

tuned internal interfaces: flags record, added kind for results; tuned;

inductive: mark internal theorems as Thm.internalK;

tuned;

export tsig_of;

clarified role of class relations

ignore mutual recursive modules