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.

made more generic;

Shortened names and added new thm.

Some streamlining of text. Theory library is now assumed to be LOCAL and not at TUM.

tuned;

tuned width of pics;

tuned;

oops;

tuned pics;

made weblint happy;

oops;

Id;

tuned; fixed links;

tuned;

main Isabelle page;

New example

Domain r, Range r replace fst``r, snd``r

increased precedence of unary minus from 80 to 100 requires a similar increase for %# and %%#

increased precedence of unary minus from 80 to 100

Charpentier laws

the Increasing operator

no need for int_0

locales now implicitly quantify over free variables

tuned current_goals_markers;

Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed

Explicit (and improved) simprules for binary arithmetic. New default simprules to eliminate (int 0) and (z + - w)

*** empty log message ***

shyps note for prim. rules;

tuned;