tuned;

updated;

some more ...;

"_not_equal" dummy constant;

updated;

some more text;

updated;

tuned;

some text on document preparation;

updated;

tuned;

updated;

mention X-Symbol; \index{Aspinall, David};

updated;

use wasysym package;

\newcommand{\isasymignore}{}, so we may use \<ignore> to disambiguate duplicate syntax declarations for demonstration purposes;

tuned;

\hfootref: use \url markup;

more on concrete syntax;

fixed \index;

tuned ``syntax (output)'';

isatool document: stderr to stdout;

tuned;

document preparation overview;

beginnings of concrete syntax;

include typedef image without path prefix!

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";