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;

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

integer compatibility: added wrapper for structure Time;

fixed use_text;

downgraded IntInf with divMod; fixed use_text;

added auto-quickcheck-time-limit;

auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;

added auto_quickcheck feature;

Norbert Schirmer: record improvements;

preliminary material for Isabelle2007;

misc tuning and update;

misc tuning and update;

misc tuning and update;

updated year to 2007;

tuned;

added some lemmas

print_state_context: local theory context, not proof context; context_position: cover Theory case as well (requires additional checkpoint);

ContextPosition.put_ctxt;

NameSelection: more interval checks;

tuned message;

turned into generic context data;

ML_setup for bind_thms;

Simplified interface for printing of interpretations.

unfold_locales workaround

Theory/context data restructured; simplified interface for printing of interpretations.

fixed dir in single-logic test

llabs/sko: removed Name.internal;

avoid unnamed infixes;

avoid internal names;

switch notification email back on

fix shell quoting confusion