NEWS
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
1999-01-27 paulson 1999-01-27 ZF typechecking
1999-01-19 paulson 1999-01-19 removal of the (thm list) argument of mk_cases
1999-01-14 nipkow 1999-01-14 More Arith.
1999-01-07 paulson 1999-01-07 ZF: the natural numbers as a datatype
1999-01-07 paulson 1999-01-07 if-then-else syntax for ZF
1999-01-06 paulson 1999-01-06 primrec, induct_tac
1999-01-05 nipkow 1999-01-05 *** empty log message ***
1999-01-04 nipkow 1999-01-04 *** empty log message ***
1998-12-11 oheimb 1998-12-11 *** empty log message ***
1998-12-04 paulson 1998-12-04 locales
1998-11-25 wenzelm 1998-11-25 removed prs / prs_fn;
1998-11-18 paulson 1998-11-18 Finally removing "Compl" from HOL
1998-10-30 wenzelm 1998-10-30 tuned current_goals_markers;
1998-10-22 wenzelm 1998-10-22 current_goals_markers;
1998-10-22 wenzelm 1998-10-22 tuned; record package;
1998-10-22 paulson 1998-10-22 locales
1998-10-21 wenzelm 1998-10-21 tuned;
1998-10-21 nipkow 1998-10-21 Tutorial
1998-10-21 wenzelm 1998-10-21 tuned (all proofs are INSTABLE by David's definition of instability);
1998-10-19 oheimb 1998-10-19 layout
1998-10-16 nipkow 1998-10-16 2. The simplifier now knows a little bit about nat-arithmetic.
1998-10-16 nipkow 1998-10-16 *** empty log message ***
1998-10-15 paulson 1998-10-15 integer simprocs
1998-09-25 wenzelm 1998-09-25 isatool logo;
1998-09-23 paulson 1998-09-23 unary minus
1998-09-21 oheimb 1998-09-21 *** empty log message ***
1998-09-21 oheimb 1998-09-21 *** empty log message ***
1998-09-15 paulson 1998-09-15 From Compl(A) to -A
1998-09-10 paulson 1998-09-10 equals0D
1998-09-04 nipkow 1998-09-04 Function 'upt'
1998-08-28 wenzelm 1998-08-28 * print mode 'emacs' reserved for Isamode;
1998-08-27 wenzelm 1998-08-27 * Pure: ML function 'theory_of' replaced by 'theory';
1998-08-24 wenzelm 1998-08-24 tuned;
1998-08-24 wenzelm 1998-08-24 isatool install;
1998-08-18 paulson 1998-08-18 ZF.thy