tuned; removed ISABELLE_SYMBOLS;

Modified proofs due to added triv_forall_equality.

Modified proofs because of added "triv_forall_equality".

Added "triv_forall_equality" to HOL_ss.

functionality added to getsettings;

removed getplatform, ISABELLE_OUTPUT_DIR;

removed getplatform, ISABELLE_OUTPUT_DIR;

removed getplatform;

integrated getplatform stuff; added ISABELLE_OUTPUT_DIR;

now falls back on ucat instead of cat;

improved usage msg;

added eq_sort (will move to sorts.ML eventually); added get_sort (handles constraints / defaults); attach_types: adapted to new get_sort;

adapted to new Syntax.read_typ;

adapted read_typ, simple_read_typ;

improved comments; raw_term_sorts: improved handling of sort constraints (consistency); added term_of_sort; renamed "_emptysort" to "_topsort"; preparations for marking of class idts;

added string_of_vname' (treats neg. index as free);

cd made readably again;

tuned;

Gradual switching to Basis Library functions nth, drop, etc.

now uses tee -i instead of perl;

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;