val copy: theory -> theory;

added unless, first;

added read_nat;

not needed in distribution

needed tidying desperately

qualified the name "restrict" since Fun.restrict exists too

moved Pi and -> (renamed funcset) to Fun.thy

the type of @evalcn was wrong

moved UNION_o to Fun.ML, since Fun.thy is no longer a parent of equalities

no longer loads Fun so that the Fun proofs can use equalities.thy

the function space operator

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;