updated;

link Types/typedef images;

Isar version; support constdefs, too;

tuned msg;

\CONSTDEFS;

tuned;

next round of updates;

Some new theorems for ordinals

tuned;

first stage of major update;

added zf.tex;

added isabelle-intro, isabelle-logics;

added \indexisarcmdof, \indexisarmethof, \indexisarattof; added \COROLLARYNAME, \COROLLARY;

New theorems by Sidi Ehmety

Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)

Added "Executing higher order logic" paper.

Added section on code generator.

tuned document sources;

'inductive_cases': support 'and' form;

* ZF/IMP: updated and converted to new-style theory format;

update by Stephan Merz;

conversion to Isar/ZF

fixed variable-clash bug in make_elim

obsolete;

tuned tracing markup;

tuned tracing_fn markup;

solve rule: tracing instead of priority;

tuned;

IMP/document/root.tex;

warn for spaces in ISABELLE_HOME;

HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);

some new theorems

conversion to Isar

tweaked the standard theorems

Resid converted to Isar/ZF

restart: sync_thy_loader instead of overly aggressive touch_all_thys; provisions for persistent sessions;

qualified point.more;

hide base name of "make", "fields", "extend", "truncate", "more", "more_update";

Theory.hide_space_i true;

hide: flag for full/base name;

HOL/record: shared operations ("more", "fields", etc.) now need to be always qualified;

tuned;

updated;

updated;

isatool browser -o;

removed Misc/Translations (text covered by Documents.thy);

Redundant patterns no longer cause errors.

Code generator now adds type constraints to val declarations (to make SML/NJ happy).

tuned;

updated;

removed Types/records.tex;

added add_fixes: derives mssing type scheme from mixfix;

fixed inst_thm: proper domain of env; flatten_expr: collective import elements over *all* imports; use ProofContext.add_fixes; disallow term bindings in locale body elements;

tuned;

added lemma;

generated text;