NEWS
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
1998-08-13 paulson 1998-08-13 stac
1998-08-08 nipkow 1998-08-08 *** empty log message ***
1998-08-06 nipkow 1998-08-06 *** empty log message ***
1998-08-06 paulson 1998-08-06 disjointness
1998-08-04 wenzelm 1998-08-04 tuned; Display.print_goals function moved to Locale.print_goals;
1998-07-31 berghofe 1998-07-31 Replaced nat.exhaustion by nat.exhaust
1998-07-30 wenzelm 1998-07-30 tuned;
1998-07-30 berghofe 1998-07-30 Adapted to new datatype package.
1998-07-28 wenzelm 1998-07-28 tuned;
1998-07-17 paulson 1998-07-17 ZF: Main, Update
1998-07-15 nipkow 1998-07-15 disjoint
1998-07-14 paulson 1998-07-14 new stac
1998-07-14 nipkow 1998-07-14 inj_on
1998-07-10 wenzelm 1998-07-10 the distribution now includes Isabelle icons: see lib/logo/isabelle-{small,tiny}.xpm;
1998-07-03 wenzelm 1998-07-03 several new basic modules made available for general use;
1998-07-03 wenzelm 1998-07-03 cleaned up;
1998-07-03 wenzelm 1998-07-03 reorganized the main HOL image;
1998-07-01 berghofe 1998-07-01 Adapted to new inductive definition package.
1998-07-01 paulson 1998-07-01 HOL-Real
1998-06-25 wenzelm 1998-06-25 simplification procedure unit_eq_proc rewrites (?x::unit) = (); quote / antiquote translations;
1998-06-24 nipkow 1998-06-24 * HOL/List: new function list_update written xs[i:=v] that updates the i-th list position. May also be iterated as in xs[i:=a,j:=b,...].
1998-06-24 paulson 1998-06-24 removed duplicate entry for Goal
1998-06-23 nipkow 1998-06-23 *** empty log message ***
1998-06-20 wenzelm 1998-06-20 renamed Thm(s) back to thm(s);
1998-06-18 wenzelm 1998-06-18 new toplevel commands `Goal' and `Goalw'; isatool fixgoal;
1998-06-18 wenzelm 1998-06-18 renamed thm(s) to Thm(s);