# HG changeset patch
# User wenzelm
# Date 869829612 -7200
# Node ID 8bd9b4b3b61de943bb40c8be244eb691b6ad0e12
# Parent  b2b9a9ddb9ccd3d3b39e88074823640396afd805
*** empty log message ***

diff -r b2b9a9ddb9cc -r 8bd9b4b3b61d NEWS
--- a/NEWS	Fri Jul 25 13:18:45 1997 +0200
+++ b/NEWS	Fri Jul 25 13:20:12 1997 +0200
@@ -11,16 +11,24 @@
 
 * removed obsolete init_pps and init_database;
 
-* defs may now be conditional;
+* defs may now be conditional; improved rewrite_goals_tac to handle
+conditional equations;
 
 * improved output of warnings / errors;
 
-* deleted the obsolete tactical STATE, which was declared by
+* deleted the obsolete tactical STATE, which was declared by:
     fun STATE tacfun st = tacfun st st;
 
-* added simplification meta rules
+* added simplification meta rules:
     (asm_)(full_)simplify: simpset -> thm -> thm;
 
+* simplifier.ML no longer part of Pure -- has to be loaded by object
+logics (again);
+
+* added prems argument to simplification procedures;
+
+
+
 New in Isabelle94-8 (May 1997)
 ------------------------------