proper escape for literal single quotes;

isabelle update -u control_cartouches;

empty -> Map.empty

more symbols;

standardized towards new-style formal comments: isabelle update_comments;

isabelle update_cartouches -c -t;

prod_case as canonical name for product type eliminator

quote "method" to allow Eisbach using this keyword;

modernized header;

folded 'Option.set' into BNF-generated 'set_option'

tuned proofs;

tuned specifications and proofs;

modernized specifications;

adjusted to changed naming convention of logical record types

modernized/unified some specifications;

"prod" and "sum" replace "*" and "+" respectively

modernized specifications

fix if-then-else parse error

cleanup type translations;

killed more recdefs

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

dropped axclass

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

Adapted to changes in cases method.

Adapted to changes in induct method.

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

Avoid record-inner constants in polymorphic definitions in Bali

The Bali package needs to insert a record extension into a type
class and define an associated polymorphic constant. There is no
elegant way to do this.

The existing approach was to insert every record extension into
the type class, defining the polymorphic constant at each layer
using inner operations created by the record package. Some of
those operations have been removed. They can be replaced by use
of record_name.extend if necessary, but we can also sidestep
this altogether.

The simpler approach here is to use defs(overloaded) once to
provide a single definition for the composition of all the type
constructors, which seems to be permitted. This gets us exactly
the fact we need, with the cost that some types that were
admitted to the type class have no definition for the constant
at all.

set intersection and union now named inter and union

Made Option a separate theory and renamed option_map to Option.map

abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);

replaced make_imp by rev_mp;

Renamed inductive2 to inductive.

resolved name clashes

Adapted to new inductive definition package.

First usable version of the new function definition package (HOL/function_packake/...).
Moved Accessible_Part.thy from Library to Main.

migrated theory headers to new format

Merged in license change from Isabelle2004

tuned HOL/record package; enabled record_upd_simproc by default.

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

Adapted to changes in Map.thy

*** 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.

Converted Fun to Isar style.
Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy.
Renamed constant "Fun.op o" to "Fun.comp"

*** empty log message ***

Cleaning up the definition of static overriding.

clarified syntax of ``long'' statements: fixes/assumes/shows;

Added check for field/method access to operational semantics and proved the acesses valid.

tuned;

Isabelle/Bali sources;