NEWS
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;
1997-12-30 nipkow 1997-12-30 nth -> !
1997-12-15 wenzelm 1997-12-15 tuned;
1997-12-11 wenzelm 1997-12-11 tuned;
1997-12-07 wenzelm 1997-12-07 tuned;
1997-12-05 wenzelm 1997-12-05 nat_cancel enabled by default;
1997-12-05 wenzelm 1997-12-05 use_thy no longer requires writable current directory;
1997-12-04 nipkow 1997-12-04 pred -> -1
1997-12-03 nipkow 1997-12-03 n ~= 0 should become 0 < n
1997-12-01 wenzelm 1997-12-01 nat_cancel simprocs;
1997-11-28 paulson 1997-11-28 addsplits now in FOL, ZF too
1997-11-21 wenzelm 1997-11-21 cd, use etc. now support path variables; changed Pure/Sequence interface;
1997-11-12 oheimb 1997-11-12 renamed split_prem_tac to split_asm_tac
1997-11-07 oheimb 1997-11-07 added split_prem_tac
1997-11-06 paulson 1997-11-06 subgoal_tac displays a warning if the new subgoal has type variables
1997-11-05 wenzelm 1997-11-05 tuned;
1997-11-05 paulson 1997-11-05 UNIV & UNION1