added ISABELLE_INSTALLFONTS;

Declaration of ccontr (classical contradiction) for HOL compatibility

Correction to Problem 24

Correction to Problem 24

Correction to Problem 24 (with unsatisfactory proof)

ex_impE was incorrectly listed as Safe

reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains

added Classlib.* and Witness.*, moved (and updated) Coind.*, Dagstuhl.*, Dlist.*, Dnat.*, Focus_ex.* and Stream.* from HOLCF/explicit_domains to here adapted several proofs; now they work again. Hope that the following strange errors (when committing) do not matter: rlog error: RCS/Classlib.ML,v: No such file or directory rlog error: RCS/Classlib.thy,v: No such file or directory rlog error: RCS/Coind.ML,v: No such file or directory rlog error: RCS/Coind.thy,v: No such file or directory rlog error: RCS/Dagstuhl.ML,v: No such file or directory rlog error: RCS/Dagstuhl.thy,v: No such file or directory rlog error: RCS/Dlist.ML,v: No such file or directory rlog error: RCS/Dlist.thy,v: No such file or directory rlog error: RCS/Dnat.ML,v: No such file or directory rlog error: RCS/Dnat.thy,v: No such file or directory rlog error: RCS/Focus_ex.ML,v: No such file or directory rlog error: RCS/Focus_ex.thy,v: No such file or directory rlog error: RCS/Stream.ML,v: No such file or directory rlog error: RCS/Stream.thy,v: No such file or directory rlog error: RCS/Witness.ML,v: No such file or directory rlog error: RCS/Witness.thy,v: No such file or directory

moved Coind.*, Dagstuhl.*, Focus_ex.* to HOLCF/ex, marked the remaining files as obsolete (new versions in HOLCF/ex)

added def_fix_ind and def_wfix_ind for convenience

added addloop (and also documentation of addsolver

changed handling of cont_lemmas and adm_lemmas

fixed getplatform call;

removed warning for unprintable chars in strings (functionality will be put into administrative script);

The redeclaration of qed_spec_mp is unnecessary because it is now declared in HOL/thy_data.ML

Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work properly in children databases

fixed problems with strange user .bashrc etc. (stty, ...);

Tidied unicity theorems

deepen_tac is NOT complete when made to apply "spec" as a safe rule\!\!

Corrected faulty comment

More news items, dating back to 1995

*** empty log message ***

*** empty log message ***

*** empty log message ***

Isabelle NEWS -- history of user-visible changes;

changed case symbol to \<Rightarrow>;

'rm -f' instead of 'mv -f';

Re-ordering of certificates so that session keys appear in decreasing order

Cosmetic improvements

'rm -f' instead of 'cp -f';

tuned;

expand shorthand goal commands;

added AxClasses test;

replaces README;

dummy file required for proper HTML generation;

removed;

removed \<mu> syntax;

added symbols syntax;

turned some consts into syntax;

Mended spelling error

Added sees_Spy_partsEs

Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()

Added warning msg when the simplifier cannot use a premise as a rewrite rule because it contains (type) unknowns.

Modified MiniML. Added W0.

Simplified proofs

Improved layout and updated comments

Improved text.

Now requests runtimes of all theories

Simplified Oops case of main theorem

Documents the new command "prlim"

Added W0 and modified MiniML.

Ball_Un -> ball_Un

The new version of MiniML including "let".

Algorithm I has not been ported to the polymorphic version yet.

Updated documentation pointers.

added gen_overwrite;

addsimps, addeqcongs: replaced @ by gen_union;

Incorporated Larry's changes.

New rewrites for bounded quantifiers

This is the old version og MiniML for the monomorphic case. The new version is now in MiniML.

Modified some defs and shortened proofs.

Now with Andy Gordon's treatment of freshness to replace newN/K

Deleted the redundant theorem subset_empty_iff (subset_empty exists already)

Added the prlim command

New miniscoping rules for the bounded quantifiers and UN/INT operators

Got rid of Alls in List. Added Ball_insert and Ball_Un in equalities.ML.

Got rid of Alls in favour of !x:set_of_list

binary oprations and relations; nat;

added termless parameter; added simplification procedures;

added term order;

improved error msg;

added datatype order;

added -? option;

replaced unit refs by 'stamp';

cleaned up (real changes next time);

make all Isabelle systems afresh;

*** empty log message ***

IsaMakefile for ZF;

Tidying of proofs. New theorems are enterred immediately into the relevant clasets or simpsets.

New theorem add_leE

New treatment of nonce creation

Removal of needless "addIs [equality]", etc.

New discussion of implicit simpsets & clasets

IsaMakefile for HOLCF;

Removal of sum_cs and eq_cs

IsaMakefile for Sequents;

IsaMakefile for CTT;

IsaMakefile for FOLP;

IsaMakefile for CCL;

IsaMakefile for LCF;

IsaMakefile for Cube;

Removed some (not all!) uses of FOL_cs

Simplification of some proofs, especially by eliminating the equality in RA2

Incorporation of HPair into Message

Default rewrite rules for quantification over Collect(A,P)

Default rewrite rules for quantification over Collect(A,P)

Now uses HPair

Tidied up the unicity proofs

Updated account of implicit simpsets and clasets

added ISABELLE, ISATOOL;

testdir: use dir without committing into database;

added dvi viewer alternative;

fixed cmp -s option;

minor tuning;

minor tuning; added Auth/Recur;

minor tuning; added thy_data.ML cladata.ML;

added stamp util;

A definition of "print", unfortunately overridden by each "open PolyML"

Implicit simpsets and clasets for FOL and ZF

Added TFL

Conversion to Basis Library (using prs instead of output)

changed xterm geometry;

removed test

testing...

testing cvs merge algorithm, 2nd

testing...

testing cvs merge algorithm

testing...

testing: last line w/o nl

testing: last line w/o nl