Attribute.thms_of;

Classical.setup, attrib_setup;

attrib_setup: rulify;

attrib_setup;

all modifiers turned into attributes; realistic method syntax; smart_simp method;

tuned attribute names; all modifiers turned into attributes; realistic method syntax;

several args parsers; realistic syntax; tuned;

tuned names;

renamed tac / etac to refine / then_refine;

add print_theorems; print_thms: handle attributes; renamed tac / etac to refine / then_refine; tuned comments; load arg: name;

add print_theorems; print_thms: handle attributes;

several args parsers; realistic syntax; attributes: transfer, RS, APP, where, standard, elimify;

several args parsers; include positions; misc tuning;

removed args, args1, thm_xname; fixed nat: Symbol.explode; name / xname: include sym_ident; keyword_symid: include ident; tuned atom_arg; support nested args;

replaced is_symid by is_sid;

renamed init_context to init;

renamed init_context to init; added read_termTs; added declare_thm;

structure PureIsar;

removed lift_modifier; removed fail; added tthms_of; added print_tthm; tuned rule;

Attribute.thms_of;

Scan.read;

added read;

tuned usage of read;

generalized JN_empty and added reachable_SKIP

removed the reference to mesontest2.ML, itself now deleted

moved some facts about Pi from ex/PiSets to Fun.ML

prefixed op;

Theory.copy;

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;

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;

tuned current_goals_markers semantics to avoid empty lines;

tidied

auto update

Some more proofs.

added nat_diff_split and a few lemmas in Trancl.