use isatool keywords -- generate from logs instead of session images;

removed duplicate target;

updated;

generate outer syntax keyword files from session logs;

export init_outer_syntax;

tuned;

report on keyword/command declarations; tuned;

tuned;

added keyword_decl, command_decl;

added class_expr; tuned;

simplified interfaces for outer syntax; tuned;

simplified interfaces for outer syntax;

updated;

(co)induct: polymorhic taking'';

added burrow_options;

tuned proofs (via polymorphic taking'');

export get_consumes;

tuned Induct interface: prefer pred'' over set'';

coinduct: instantiation refers to suffix of main prop (major premise or conclusion); tuned;

tuned induct etc.;

execute/system: non-critical;

subtract: minor performance tuning;

cover only .gz files;

metis method: used theorems

filtering out some package theorems

added lemmas

single-threaded profiling;

tuned;

Name.uu, Name.aT;

added uu, aT;

replaced literal 'a by Name.aT;

replaced AxClass.param_tyvarname by Name.aT;

added nth_drop

tuned datatype_codegen setup

certificates for code generator case expressions

added illustrative diagnostics

clarified declarations in class ord

concept for exceptions

clarified name suffix

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;