new rule rev_bexI

new theorems Domain_Union, Range_Union

removed duplicate contrapos;

enum: !!! after seperator;

excursion: ERROR_MESSAGE; exn_message: ERROR;

qed: kind_name (again);

show_tags flag;

new theorem INT_Un

better version of Image_diag

tactical CHANGED now uses alpha-eta conversion, not alpha conversion Streamlined code

Renamed subset_Sigma_llist to subset_Times_llist

new theorems about diag

fixed declatation of patterns and skolem;

tuned print_state; changed solve semantics: support back-pressure of asms (cut, def etc.);

tuned welcome msg;

added restart;

added exception RESTART;

proof_general_trans (experimental);

replaced wakeup by decorate_prompt_fn;

eliminated "Trying to recover ..." msg;

added oct_char;

method brute_force = ALLGOALS force_tac;

*** empty log message ***

At last: linear arithmetic for nat!

Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.

fixed a link

added Real/Hyperreal

Addition of Hyperreal theories Zorn and Filter

moved diag (diagonal relation) from Univ to Relation

tidied up list definitions, using type 'a option instead of unit + 'a, also using real typedefs instead of faking them with extra rules

tuning to assimiliate it with PhD;

Added a general refutation tactic which works by putting things into nnf first.

Added filter_prems_tac

removed prs / prs_fn;

guarantees laws

simplified ensures_UNIV

new thms for invariant

new theorem program_equalityE

renamed vars

image_id in simpset

removed prs / prs_fn (broken, because it did not include \n in its semantics, forcing writeln to add one uncoditionally); replaced prs_fn by writeln fn;

eliminated ISABELLE_INTERFACE_OPTIONS;

improved comment; removed ISABELLE_INTERFACE_OPTIONS; added ProofGeneral;

replaced prs by std_output;

replaced prs by writeln;

replaced prs by std_output / writeln;

comment parser;

add_text, add_chapter etc.: dummy;

chapter etc. headings; use, use_thy, cd: name;

tuned space;

replaced prs by writeln;

removed redirect_to_latex stuff;

Isar.main();

setup Blast.setup; setup Clasimp.setup;

added commands;

added isar.ML;

Isabelle/Isar main interface.

fixed prefix_lines: *separate* by \n;

added Isar/isar.ML;

fixed links

print_state hook, obeys Goals.current_goals_markers by default;

print_state: use begin_goal from Goals.current_goals_markers;

added undos, redos;

tty: issue wakeup;

std_output, prefix_lines;

better miniscoping rules: the premise C~={} is not good because Safe_tac eliminates such assumptions.

fixed method syntax;

break: exhibit state stack;

match_bind: 'as' patterns; statements: 'is' patterns;

let: 'as' patterns; statements: propp ('is' patterns);

match_bind(_i): 'as' patterns; assume, theorem, show etc.: propp; tuned qed msg;

term_pat vs. prop_pat; added bind_propp(_i); assume: propp;

term_pat vs. prop_pat;

no warning for "it" theorems;

tidied

Finally removing "Compl" from HOL

exn_message FAIL;

blast: cla_method';

export simp_modifiers;

expoer cla_method('), cla_modifiers;

method setup;

tuned comments;

'prop', 'term', 'typ';

load;

export exn_message;

removed trace;

BREAK: include state; report Attrib.ATTRIB_FAIL, Method.METHOD_FAIL;

have_tthms; assume: store actual asms;

PureThy.default_name; have_tthms;

generalized (opt_)thm_name; xthm, xthms1;

exception METHOD_FAIL;

added have_theorems, have_lemmas, have_facts; tuned from_facts; Theory.apply replaced by Library.apply;

added 'theorems', 'lemmas', 'note'; tuned 'thm';

break: exhibit state; removed print_thm;

exception ATTRIB_FAIL; local_attribute'; removed 'lemma', 'assumption'; added 'where', 'with';

removed trace;

Symbol.space;

space;

val spc: int -> T;

added default_name; added have_tthmss;

Drule.rev_triv_goal;

Theory.apply replaced by Library.apply;

val apply: ('a -> 'a) list -> 'a -> 'a; val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b;

export vars_of and friends; open BasicDrule only;

Pretty.spc;

added pretty_tthms, print_tthms; tuned apply(s);

new theory UNITY/PPROD

new theory PPROD

a faster proof

removed genelim.ML;

thm, thms;

added print_thm;

made SML/NJ happy;

added oo, ooo (*concatenation: 2 and 3 args*);

Attribute.tthms_of; Theory.copy;

Attribute.tthms_of;

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.

ML_SYSTEM=polyml-3.1;

tuned checklist;

official release;

ML_SYSTEM factory default;