more symbols;

standardized towards new-style formal comments: isabelle update_comments;

isabelle update_cartouches -c -t;

clarified print modes;

prefer tactics with explicit context;

modernized header;

simplified statements and proofs;

tuned white space;

eliminated obsolete "standard";

robustified proof

modernized/unified some specifications;

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

removed obsolete CVS Ids;

modernized syntax translations, using mostly abbreviation/notation;
minor tuning;

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

avoid internal names;

replaced make_imp by rev_mp;

Renamed inductive2 to inductive.

Adapted to new inductive definition package.

removed or modified some instances of [iff]

migrated theory headers to new format

Merged in license change from Isabelle2004

reimplementation of HOL records; only one type is created for
each record extension, instead of one type for each field. See NEWS.

*** empty log message ***

"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.

GPLed;

tuned header;

Isabelle/Bali sources;