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;

supplanted by Records.thy;

some text;

\usepackage{marvosym};

document/Records.tex;