NEWS
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
1997-11-04 wenzelm 1997-11-04 tuned;
1997-11-04 oheimb 1997-11-04 *** empty log message ***
1997-11-04 wenzelm 1997-11-04 tuned;
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-03 nipkow 1997-11-03 *** empty log message ***
1997-10-30 nipkow 1997-10-30 *** empty log message ***
1997-10-24 wenzelm 1997-10-24 tuned;
1997-10-24 nipkow 1997-10-24 HOL/Map
1997-10-21 wenzelm 1997-10-21 improved handling of draft signatures / theories; draft thms (and ctyps, cterms) are automatically promoted to real ones;
1997-10-21 nipkow 1997-10-21 typo
1997-10-20 wenzelm 1997-10-20 tuned qualified names;
1997-10-18 nipkow 1997-10-18 addsplits
1997-10-16 wenzelm 1997-10-16 tuned;
1997-10-15 wenzelm 1997-10-15 slightly changed interfaces for oracles;
1997-10-14 wenzelm 1997-10-14 browser info;
1997-10-14 paulson 1997-10-14 rearranged and added TLA
1997-10-13 wenzelm 1997-10-13 print_goals: optional output of const types (set show_consts);
1997-10-13 wenzelm 1997-10-13 hierachically structured name spaces;
1997-10-09 wenzelm 1997-10-09 no longer handles consts "" -- use syntax instead; pretty printer: changed order of mixfix annotation preference (again!);
1997-09-29 wenzelm 1997-09-29 tuned;