NEWS
2002-08-27 wenzelm 2002-08-27 * Pure: disallow duplicate fact bindings within new-style theory files;
2002-08-27 wenzelm 2002-08-27 * Isar: preview of problems to finish 'show' now produce an error
2002-08-23 nipkow 2002-08-23 *** empty log message ***
2002-08-13 nipkow 2002-08-13 *** empty log message ***
2002-08-12 nipkow 2002-08-12 *** empty log message ***
2002-08-08 wenzelm 2002-08-08 * Pure: improved error reporting of simprocs; tuned;
2002-08-06 wenzelm 2002-08-06 * Provers: Simplifier.simproc(_i) now provide sane interface for setting up simprocs;
2002-08-06 wenzelm 2002-08-06 * Pure: predefined locales "var" and "struct" are useful for sharing parameters (as in CASL, for example); just specify something like ``var x + var y + struct M'' as import;
2002-08-02 wenzelm 2002-08-02 typedef: "open" option;
2002-07-26 wenzelm 2002-07-26 support for split assumptions in cases (hyps vs. prems);
2002-07-24 wenzelm 2002-07-24 * Pure: locale specifications now produce predicate definitions;
2002-07-11 nipkow 2002-07-11 *** empty log message ***
2002-07-02 wenzelm 2002-07-02 thms_containing: optional limit argument;
2002-07-02 wenzelm 2002-07-02 * improved thms_containing: proper indexing of facts instead of raw theorems; check validity of results wrt. current name space; include local facts of proof configuration (also covers active locales);
2002-05-31 nipkow 2002-05-31 *** empty log message ***
2002-05-30 nipkow 2002-05-30 *** empty log message ***
2002-05-17 nipkow 2002-05-17 *** empty log message ***
2002-03-07 wenzelm 2002-03-07 tuned;
2002-03-05 wenzelm 2002-03-05 tuned;
2002-03-05 berghofe 2002-03-05 Added two paragraphs on "rules" method and code generator.
2002-02-28 wenzelm 2002-02-28 fixed date;
2002-02-27 wenzelm 2002-02-27 tuned;
2002-02-21 wenzelm 2002-02-21 * HOL: removed obsolete theorem "optionE";
2002-02-21 wenzelm 2002-02-21 * HOL: removed obsolete theorem "optionE";
2002-02-19 wenzelm 2002-02-19 "isatool usedir -D output HOL Test && isatool document Test/output";
2002-02-14 nipkow 2002-02-14 *** empty log message ***
2002-02-12 wenzelm 2002-02-12 * Isar/Pure: marginal comments ``--'' may now occur just anywhere in the text;
2002-01-26 wenzelm 2002-01-26 Isar cases/induct: no backtracking;
2002-01-25 paulson 2002-01-25 ZF
2002-01-23 wenzelm 2002-01-23 * HOL: nat_number_of;
2002-01-21 wenzelm 2002-01-21 * Pure/show_hyps reset by default (in accordance to existing Isar practice);
2002-01-16 paulson 2002-01-16 Isar version of ZF/AC
2002-01-15 wenzelm 2002-01-15 tuned;
2002-01-15 wenzelm 2002-01-15 Isar: undeclared rule case names default to numbers 1, 2, 3, ...;
2002-01-14 wenzelm 2002-01-14 * system: reduced base memory usage by Poly/ML (approx. 20 MB instead of 40 MB), cf. ML_OPTIONS;
2002-01-13 wenzelm 2002-01-13 * HOL: symbolic syntax for x^2 (numeral 2);
2002-01-13 wenzelm 2002-01-13 HOL-Real/Complex_Numbers;
2002-01-12 wenzelm 2002-01-12 tuned;
2002-01-11 wenzelm 2002-01-11 Isabelle2002 (January 2002);
2002-01-11 wenzelm 2002-01-11 * Pure: localized 'lemmas', 'theorems', 'declare';
2002-01-09 wenzelm 2002-01-09 * added \<euro> symbol; * HOL-Hyperreal is now a logic image; * isatool latex no longer depends on changed TEXINPUTS;
2002-01-03 wenzelm 2002-01-03 tuned;
2001-12-29 wenzelm 2001-12-29 * ZF/IMP: updated and converted to new-style theory format;
2001-12-27 wenzelm 2001-12-27 HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
2001-12-21 wenzelm 2001-12-21 HOL/record: shared operations ("more", "fields", etc.) now need to be always qualified;
2001-12-20 nipkow 2001-12-20 *** empty log message ***
2001-12-20 paulson 2001-12-20 ZF/Main
2001-12-18 wenzelm 2001-12-18 * system: tested support for MacOS X;
2001-12-13 nipkow 2001-12-13 *** empty log message ***
2001-12-11 wenzelm 2001-12-11 tuned;
2001-12-11 wenzelm 2001-12-11 isatools "symbolinput" and "nonascii" have disappeared;
2001-12-10 wenzelm 2001-12-10 * HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam" -- INCOMPATIBILITY;
2001-12-06 wenzelm 2001-12-06 * Pure/obtain: "thesis" now internal (use ?thesis); * Pure: generic 'sym' / 'symmetric' attributes; * Provers/classical: 'swapped' attribute; * HOL: proper rules less_induct and wf_induct_rule;
2001-12-05 wenzelm 2001-12-05 * Pure/Provers/classical: simplified integration with pure rule attributes and methods;
2001-12-01 wenzelm 2001-12-01 * HOL: the class of all HOL types is now called "type" rather than "term"; INCOMPATIBILITY, need to adapt references to this type class in axclass/classes, instance/arities, and (usually rare) occurrences in typings (of consts etc.); internally the class is called "HOL.type", ML programs should refer to HOLogic.typeS;
2001-11-28 wenzelm 2001-11-28 * Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode; * Pure/syntax: "x::_::foo" sort constraints;
2001-11-24 wenzelm 2001-11-24 tuned;
2001-11-20 wenzelm 2001-11-20 * HOL/record: cases/induct for more parts; * syntax: prefer later print_translation functions;
2001-11-20 paulson 2001-11-20 Hyperreal
2001-11-15 wenzelm 2001-11-15 * ZF: new-style theory commands '(co)inductive', '(co)datatype', 'rep_datatype', 'inductive_cases'; also methods 'ind_cases', 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');