*** empty log message ***
authorwenzelm
Fri Jul 25 13:20:12 1997 +0200 (1997-07-25)
changeset 35798bd9b4b3b61d
parent 3578 b2b9a9ddb9cc
child 3580 04c6ae944b5e
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Fri Jul 25 13:18:45 1997 +0200
     1.2 +++ b/NEWS	Fri Jul 25 13:20:12 1997 +0200
     1.3 @@ -11,16 +11,24 @@
     1.4  
     1.5  * removed obsolete init_pps and init_database;
     1.6  
     1.7 -* defs may now be conditional;
     1.8 +* defs may now be conditional; improved rewrite_goals_tac to handle
     1.9 +conditional equations;
    1.10  
    1.11  * improved output of warnings / errors;
    1.12  
    1.13 -* deleted the obsolete tactical STATE, which was declared by
    1.14 +* deleted the obsolete tactical STATE, which was declared by:
    1.15      fun STATE tacfun st = tacfun st st;
    1.16  
    1.17 -* added simplification meta rules
    1.18 +* added simplification meta rules:
    1.19      (asm_)(full_)simplify: simpset -> thm -> thm;
    1.20  
    1.21 +* simplifier.ML no longer part of Pure -- has to be loaded by object
    1.22 +logics (again);
    1.23 +
    1.24 +* added prems argument to simplification procedures;
    1.25 +
    1.26 +
    1.27 +
    1.28  New in Isabelle94-8 (May 1997)
    1.29  ------------------------------
    1.30