1.1 --- a/NEWS	Thu Sep 25 12:32:14 1997 +0200
     1.2 +++ b/NEWS	Thu Sep 25 13:23:41 1997 +0200
     1.3 @@ -5,16 +5,49 @@
     1.4  New in Isabelle???? (DATE ????)
     1.5  -------------------------------
     1.6  
     1.7 -* Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
     1.8 +*** General Changes ***
     1.9  
    1.10 -* HOLCF: fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
    1.11 +* improved output of warnings / errors;
    1.12  
    1.13 -* added extended adm_tac to simplifier in HOLCF. Is now capable to discharge
    1.14 -  adm (%x. P (t x)), where P is chainfinite and t continuous.
    1.15 +* removed old README and Makefiles;
    1.16 +
    1.17 +* defs may now be conditional; improved rewrite_goals_tac to handle
    1.18 +conditional equations;
    1.19  
    1.20  * replaced print_goals_ref hook by print_current_goals_fn and
    1.21    result_error_fn;
    1.22  
    1.23 +* removed obsolete init_pps and init_database;
    1.24 +
    1.25 +* deleted the obsolete tactical STATE, which was declared by
    1.26 +    fun STATE tacfun st = tacfun st st;
    1.27 +
    1.28 +
    1.29 +*** Classical Reasoner ***
    1.30 +
    1.31 +* Clarify_tac. clarify_tac, clarify_step_tac, Clarify_step_tac :
    1.32 +   new tactics that use classical reasoning to simplify a subgoal 
    1.33 +   without splitting it into several subgoals;
    1.34 +
    1.35 +
    1.36 +*** Simplifier ***
    1.37 +
    1.38 +* added simplification meta rules:
    1.39 +    (asm_)(full_)simplify: simpset -> thm -> thm;
    1.40 +
    1.41 +* simplifier.ML no longer part of Pure -- has to be loaded by object
    1.42 +logics (again);
    1.43 +
    1.44 +* added prems argument to simplification procedures;
    1.45 +
    1.46 +
    1.47 +*** Syntax ***
    1.48 +
    1.49 +* Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
    1.50 +
    1.51 +
    1.52 +*** HOL ***
    1.53 +
    1.54  * HOL/simplifier: terms of the form
    1.55    `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)
    1.56    are rewritten to
    1.57 @@ -23,25 +56,13 @@
    1.58  * HOL/Lists: the function "set_of_list" has been renamed "set" (and its 
    1.59    theorems too);
    1.60  
    1.61 -* removed old README and Makefiles;
    1.62  
    1.63 -* removed obsolete init_pps and init_database;
    1.64 +*** HOLCF ***
    1.65  
    1.66 -* defs may now be conditional; improved rewrite_goals_tac to handle
    1.67 -conditional equations;
    1.68 +* HOLCF: fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
    1.69  
    1.70 -* improved output of warnings / errors;
    1.71 -
    1.72 -* deleted the obsolete tactical STATE, which was declared by:
    1.73 -    fun STATE tacfun st = tacfun st st;
    1.74 -
    1.75 -* added simplification meta rules:
    1.76 -    (asm_)(full_)simplify: simpset -> thm -> thm;
    1.77 -
    1.78 -* simplifier.ML no longer part of Pure -- has to be loaded by object
    1.79 -logics (again);
    1.80 -
    1.81 -* added prems argument to simplification procedures;
    1.82 +* added extended adm_tac to simplifier in HOLCF.  Can now discharge
    1.83 +  adm (%x. P (t x)), where P is chainfinite and t continuous.
    1.84  
    1.85  
    1.86