NEWS
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
1999-03-17 wenzelm 1999-03-17 HOL/typedef: fixed type inference for representing set; AxClass.axclass_tac lost the theory argument;
1999-03-10 wenzelm 1999-03-10 updated;
1999-02-11 wenzelm 1999-02-11 Symbol.output subject to print mode;
1999-02-11 wenzelm 1999-02-11 tuned; TLA update;
1999-02-08 wenzelm 1999-02-08 path element specification '~~' refers to '$ISABELLE_HOME';
1999-02-03 paulson 1999-02-03 inj
1999-01-27 nipkow 1999-01-27 arith_tac for min/max