NEWS
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);
1998-06-17 nipkow 1998-06-17 Goal and Goalw
1998-06-10 wenzelm 1998-06-10 new type-safe user interface for theory data;
1998-06-05 wenzelm 1998-06-05 * improved the theory data mechanism to support real encapsulation; main change of the internal interfaces: data kind name (string) replaced by private Object.kind, acting as authorization key;
1998-05-28 wenzelm 1998-05-28 tuned header;
1998-05-14 oheimb 1998-05-14 extended addsplits and delsplits to handle also split rules for assumptions extended const_of_split_thm, renamed it to split_thm_info
1998-05-13 wenzelm 1998-05-13 HOL/record: now includes concrete syntax for record terms;
1998-05-06 paulson 1998-05-06 HOL/Update
1998-05-01 nipkow 1998-05-01 *** empty log message ***
1998-05-01 paulson 1998-05-01 "let" is no longer restricted to FOL terms and allows any logical terms
1998-04-29 wenzelm 1998-04-29 new theory section 'setup';
1998-04-29 wenzelm 1998-04-29 new theory section 'nonterminals';
1998-04-29 wenzelm 1998-04-29 *** empty log message ***
1998-04-27 oheimb 1998-04-27 cleanup for split_all_tac as wrapper in claset()
1998-04-27 nipkow 1998-04-27 *** empty log message ***
1998-04-24 oheimb 1998-04-24 improved split_all_tac significantly
1998-04-24 paulson 1998-04-24 tidied; div & mod
1998-04-24 oheimb 1998-04-24 *** empty log message ***
1998-04-10 paulson 1998-04-10 bug fixes
1998-04-07 oheimb 1998-04-07 *** empty log message ***
1998-04-03 paulson 1998-04-03 UNITY
1998-04-02 oheimb 1998-04-02 *** empty log message ***
1998-03-16 paulson 1998-03-16 inverse -> converse
1998-03-12 oheimb 1998-03-12 renamed not1_or to disj_not1, not2_or to disj_not2
1998-03-11 nipkow 1998-03-11 Simplifier
1998-03-09 wenzelm 1998-03-09 removed pred;
1998-03-06 nipkow 1998-03-06 *** empty log message ***
1998-02-27 paulson 1998-02-27 Vimage
1998-02-26 wenzelm 1998-02-26 *** empty log message ***
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1998-01-14 wenzelm 1998-01-14 HOL/record;