NEWS
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
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;