isabelle: Changelog

Modified and shortened adm_disj lemmas.

Deleted a useless definition

Added optimization: do nothing for empty list

A bit more pattern-matching in eta_contract

Tidying and a corrected comment

Added a new challenge problem

Updated documentation of IFOL_ss

Strengthened warnings concerning topthm(), etc.

New class "order" and accompanying changes.

New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.

TFL: missing -q option!

tuned names: partial order, linear order;

tuned startup; semi fix of piping-quit peoblem (should work on systems with *real& sh);

Renamed structure Int (intuitionistic prover) to IntPr to prevent clash with Basis Library structure Int

Renamed structure Int (intuitionistic prover) to IntPr

Renamed structure Int (intuitionistic prover) to IntPr to prevent clash with Basis Library structure Int

removed ISABELLE_INTERFACE_OPTIONS;

tuned; removed ISABELLE_INTERFACE_OPTIONS;

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;

integrated getplatform stuff; added ISABELLE_OUTPUT_DIR;

now falls back on ucat instead of cat;

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;

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 (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