now uses ISABELLE_INSTALLFONTS;

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