1997-02-07 nipkow 1997-02-07 Modified proofs due to added triv_forall_equality.
1997-02-07 nipkow 1997-02-07 Modified proofs because of added "triv_forall_equality".
1997-02-07 nipkow 1997-02-07 Added "triv_forall_equality" to HOL_ss.
1997-02-06 wenzelm 1997-02-06 functionality added to getsettings;
1997-02-06 wenzelm 1997-02-06 removed getplatform, ISABELLE_OUTPUT_DIR;
1997-02-06 wenzelm 1997-02-06 removed getplatform, ISABELLE_OUTPUT_DIR;
1997-02-06 wenzelm 1997-02-06 removed getplatform;
1997-02-06 wenzelm 1997-02-06 integrated getplatform stuff; added ISABELLE_OUTPUT_DIR;
1997-02-06 wenzelm 1997-02-06 now falls back on ucat instead of cat;
1997-02-06 wenzelm 1997-02-06 improved usage msg;
1997-02-06 wenzelm 1997-02-06 added eq_sort (will move to sorts.ML eventually); added get_sort (handles constraints / defaults); attach_types: adapted to new get_sort;
1997-02-06 wenzelm 1997-02-06 adapted to new Syntax.read_typ;
1997-02-06 wenzelm 1997-02-06 adapted read_typ, simple_read_typ;
1997-02-06 wenzelm 1997-02-06 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;
1997-02-06 wenzelm 1997-02-06 added string_of_vname' (treats neg. index as free);
1997-02-06 wenzelm 1997-02-06 cd made readably again;
1997-02-05 wenzelm 1997-02-05 tuned;
1997-02-04 paulson 1997-02-04 Gradual switching to Basis Library functions nth, drop, etc.
1997-02-04 wenzelm 1997-02-04 now uses tee -i instead of perl;
1997-02-04 wenzelm 1997-02-04 now uses ISABELLE_INSTALLFONTS;
1997-02-04 wenzelm 1997-02-04 added ISABELLE_INSTALLFONTS;
1997-01-31 paulson 1997-01-31 Declaration of ccontr (classical contradiction) for HOL compatibility
1997-01-31 paulson 1997-01-31 Correction to Problem 24
1997-01-31 paulson 1997-01-31 Correction to Problem 24
1997-01-31 paulson 1997-01-31 Correction to Problem 24 (with unsatisfactory proof)
1997-01-31 paulson 1997-01-31 ex_impE was incorrectly listed as Safe
1997-01-31 oheimb 1997-01-31 reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
1997-01-31 oheimb 1997-01-31 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
1997-01-31 oheimb 1997-01-31 moved Coind.*, Dagstuhl.*, Focus_ex.* to HOLCF/ex, marked the remaining files as obsolete (new versions in HOLCF/ex)
1997-01-31 oheimb 1997-01-31 added def_fix_ind and def_wfix_ind for convenience
1997-01-31 oheimb 1997-01-31 added addloop (and also documentation of addsolver
1997-01-31 oheimb 1997-01-31 changed handling of cont_lemmas and adm_lemmas
1997-01-29 wenzelm 1997-01-29 fixed getplatform call;
1997-01-29 wenzelm 1997-01-29 removed warning for unprintable chars in strings (functionality will be put into administrative script);
1997-01-29 paulson 1997-01-29 The redeclaration of qed_spec_mp is unnecessary because it is now declared in HOL/thy_data.ML
1997-01-29 paulson 1997-01-29 Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work properly in children databases
1997-01-28 wenzelm 1997-01-28 fixed problems with strange user .bashrc etc. (stty, ...);
1997-01-27 paulson 1997-01-27 Tidied unicity theorems
1997-01-27 paulson 1997-01-27 deepen_tac is NOT complete when made to apply "spec" as a safe rule\!\!
1997-01-27 paulson 1997-01-27 Corrected faulty comment
1997-01-27 paulson 1997-01-27 More news items, dating back to 1995
1997-01-27 wenzelm 1997-01-27 *** empty log message ***
1997-01-24 wenzelm 1997-01-24 *** empty log message ***
1997-01-24 wenzelm 1997-01-24 *** empty log message ***
1997-01-24 wenzelm 1997-01-24 Isabelle NEWS -- history of user-visible changes;
1997-01-24 wenzelm 1997-01-24 changed case symbol to \<Rightarrow>;
1997-01-23 wenzelm 1997-01-23 'rm -f' instead of 'mv -f';
1997-01-23 paulson 1997-01-23 Re-ordering of certificates so that session keys appear in decreasing order
1997-01-23 paulson 1997-01-23 Cosmetic improvements
1997-01-23 wenzelm 1997-01-23 'rm -f' instead of 'cp -f';
1997-01-23 wenzelm 1997-01-23 tuned;
1997-01-23 wenzelm 1997-01-23 expand shorthand goal commands;
1997-01-23 wenzelm 1997-01-23 added AxClasses test;
1997-01-23 wenzelm 1997-01-23 replaces README;
1997-01-23 wenzelm 1997-01-23 dummy file required for proper HTML generation;
1997-01-23 wenzelm 1997-01-23 removed;
1997-01-23 wenzelm 1997-01-23 removed \<mu> syntax;
1997-01-23 wenzelm 1997-01-23 added symbols syntax;
1997-01-23 wenzelm 1997-01-23 turned some consts into syntax;
1997-01-23 paulson 1997-01-23 Mended spelling error