NEWS
2000-03-10 nipkow 2000-03-10 cases_tac
2000-03-09 paulson 2000-03-09 Factorization
2000-03-08 wenzelm 2000-03-08 * isatool mkdir provides easy setup of Isabelle session directories, including proper documents; * generated LaTeX sources are now deleted after successful run (isatool document -c); may retain a copy somewhere else via -D option of isatool usedir; * old-style theories now produce (crude) LaTeX sources as well; * compression of ML heaps images may now be controlled via -c option of isabelle and isatool usedir;
2000-02-22 wenzelm 2000-02-22 * Pure now provides its own version of intro/elim/dest attributes; useful for building new logics, but beware of confusion with the Provers/classical ones! * HOL: removed "case_split" thm binding, should use "cases" proof method anyway; * tuned syntax of "induct" method; * new "cases" method for propositions, inductive sets and types; * HOL/records: admit "r" as field name;
2000-02-21 wenzelm 2000-02-21 HOL/record: fixed select-update simplification procedure to handle extended records as well;
2000-02-07 wenzelm 2000-02-07 intro/elim/dest attributes: changed ! / !! flags to ? / ??;
2000-02-02 wenzelm 2000-02-02 nat as names; obtain; tuned;
1999-11-12 wenzelm 1999-11-12 tuned;
1999-11-11 paulson 1999-11-11 HOL changes
1999-11-11 wenzelm 1999-11-11 header;
1999-10-30 wenzelm 1999-10-30 Isabelle99;
1999-10-22 wenzelm 1999-10-22 tuned simplifier trace output; new flag debug_simp
1999-10-20 wenzelm 1999-10-20 the settings environment is now statically scoped; tuned;
1999-10-14 wenzelm 1999-10-14 document preparation based on (PDF)LaTeX;
1999-10-13 berghofe 1999-10-13 Eliminated mutual_induct_tac.
1999-10-08 wenzelm 1999-10-08 theorem database now also indexes constants "Trueprop", "all", "==>", "=="; thus thms_containing, findI etc. may retrieve more rules;
1999-10-08 wenzelm 1999-10-08 tuned;
1999-10-07 berghofe 1999-10-07 Documented changes to HOL/inductive and function thm_deps.
1999-10-04 wenzelm 1999-10-04 added BVC;
1999-09-29 wenzelm 1999-09-29 proper handling of dangling sort hypotheses (at last!);
1999-09-28 nipkow 1999-09-28 incompatibility solver
1999-09-24 wenzelm 1999-09-24 * HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar) -- by Gertrud Bauer;
1999-09-24 wenzelm 1999-09-24 tuned;
1999-09-06 oheimb 1999-09-06 *** empty log message ***
1999-09-03 wenzelm 1999-09-03 added bind_thms;
1999-09-03 paulson 1999-09-03 new SVC url
1999-09-01 wenzelm 1999-09-01 structures Vartab / Termtab (instances of TableFun);
1999-08-23 wenzelm 1999-08-23 tuned;
1999-08-23 wenzelm 1999-08-23 record_simproc;
1999-08-23 nipkow 1999-08-23 simplifier flex heads.
1999-08-23 berghofe 1999-08-23 Moved sum_case to theory HOL/Datatype.
1999-08-21 wenzelm 1999-08-21 real numerals;
1999-08-19 wenzelm 1999-08-19 * HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;
1999-08-19 paulson 1999-08-19 defer_recdef
1999-08-19 wenzelm 1999-08-19 tuned;
1999-08-18 wenzelm 1999-08-18 sum_case renamed to basic_sum_case;
1999-08-18 wenzelm 1999-08-18 replaced 'ProofGeneral' by 'Proof General';
1999-08-17 wenzelm 1999-08-17 replaced HOL_quantifiers flag by "HOL" print mode; simplified HOL basic syntax (more orthogonal);
1999-08-16 wenzelm 1999-08-16 tuned;
1999-08-16 wenzelm 1999-08-16 tuned;
1999-08-11 nipkow 1999-08-11 Removed * reset HOL_quantifiers by default, i.e. quantifiers are printed as ALL/EX rather than !/?;
1999-08-09 wenzelm 1999-08-09 theory loader actions;
1999-08-03 paulson 1999-08-03 SVC
1999-07-28 wenzelm 1999-07-28 HOL-Real target now builds an actual image;
1999-07-28 paulson 1999-07-28 LK
1999-07-19 berghofe 1999-07-19 Datatype package now handles arbitrarily branching datatypes.
1999-07-08 wenzelm 1999-07-08 theorems involving oracles are now printed with a suffixed [!];
1999-07-08 paulson 1999-07-08 integer division
1999-06-07 wenzelm 1999-06-07 reset HOL_quantifiers by default;
1999-05-31 wenzelm 1999-05-31 Isabelle manuals now also available as PDF;
1999-05-18 wenzelm 1999-05-18 tuned;
1999-05-03 wenzelm 1999-05-03 tuned;
1999-04-27 wenzelm 1999-04-27 tuned;
1999-04-22 wenzelm 1999-04-22 recdef (TFL) now requires theory Recdef;
1999-04-21 wenzelm 1999-04-21 Isamode 2.6 requires patch;
1999-04-16 wenzelm 1999-04-16 loadpath replaced;
1999-04-14 wenzelm 1999-04-14 tuned;
1999-04-13 wenzelm 1999-04-13 improved isatool install;
1999-04-12 wenzelm 1999-04-12 ML_PLATFORM;
1999-03-18 nipkow 1999-03-18 * New bounded quantifier syntax (input only): ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P