New section on advanced datatypes.

*** empty log message ***

mesontest2.ML was never needed in the distribution

changed inverse syntax from x-| to i(x)

proved surjI

tidied

Big simplification of proofs. Deleted lots of unnecessary theorems

tiny changes;

changed to a link;

local simpset theory data; simp add / del attributes; smart_simp_tac and method;

local claset theory data; intro, elim, dest, del attributes; single_tac and method; fast, best etc. methods;

Object logic specific operations.

Isar setups;

added metacuts_tac;

removed local_theory;

exnMessage Interrupt;

added lift_modifier, rule;

added Isar;

added Isar/;

Pure outer syntax.

Non-logical toplevel commands.

Derived theory operations.

The global Isabelle/Isar outer syntax.

The Isabelle/Isar toplevel.

Histories of proof states, with undo / redo and prev / back.

Generic parsers for Isabelle/Isar outer syntax.

Outer lexical syntax for Isabelle/Isar.

Proof methods.

Symbolic theorem attributes.

Concrete argument syntax (for attributes, methods etc.).

Type-safe interface for proof context data.

Proof states and methods.

Proof context information.

Isar -- Intelligible Semi-Automated Reasoning for Isabelle.

Check release name and date in NEWS!

smart interrupt handler;

option -I: startup Isar interaction mode;

isabelle -I;

fake interrupt handler;

simple interrupt_handler;

new Domain/Range rules

new TIMES/Sigma rules

removed obsolete comment and "open" declaration

"Subscribe" link

spell check;

tuned;

added mailing list, removed mirrors;

Revising the Client proof as suggested by Michel Charpentier. New lemmas about composition (in Union.ML), etc. Also changed "length" to "size" because it is displayed as "size" in any event.