# HG changeset patch
# User paulson
# Date 875186621 -7200
# Node ID 6e074b41c73536b56e2b14eb6badbe17d0a99181
# Parent  ab3b4ceb61dc037c71cd74fabbc833705dd4e03f
Clarify_tac; general reorganization

diff -r ab3b4ceb61dc -r 6e074b41c735 NEWS
--- a/NEWS	Thu Sep 25 12:32:14 1997 +0200
+++ b/NEWS	Thu Sep 25 13:23:41 1997 +0200
@@ -5,16 +5,49 @@
 New in Isabelle???? (DATE ????)
 -------------------------------
 
-* Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
+*** General Changes ***
+
+* improved output of warnings / errors;
 
-* HOLCF: fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
+* removed old README and Makefiles;
 
-* added extended adm_tac to simplifier in HOLCF. Is now capable to discharge
-  adm (%x. P (t x)), where P is chainfinite and t continuous.
+* defs may now be conditional; improved rewrite_goals_tac to handle
+conditional equations;
 
 * replaced print_goals_ref hook by print_current_goals_fn and
   result_error_fn;
 
+* removed obsolete init_pps and init_database;
+
+* deleted the obsolete tactical STATE, which was declared by
+    fun STATE tacfun st = tacfun st st;
+
+
+*** Classical Reasoner ***
+
+* Clarify_tac. clarify_tac, clarify_step_tac, Clarify_step_tac :
+   new tactics that use classical reasoning to simplify a subgoal 
+   without splitting it into several subgoals;
+
+
+*** Simplifier ***
+
+* 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;
+
+
+*** Syntax ***
+
+* Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
+
+
+*** HOL ***
+
 * HOL/simplifier: terms of the form
   `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)
   are rewritten to
@@ -23,25 +56,13 @@
 * HOL/Lists: the function "set_of_list" has been renamed "set" (and its 
   theorems too);
 
-* removed old README and Makefiles;
 
-* removed obsolete init_pps and init_database;
-
-* defs may now be conditional; improved rewrite_goals_tac to handle
-conditional equations;
-
-* improved output of warnings / errors;
+*** HOLCF ***
 
-* deleted the obsolete tactical STATE, which was declared by:
-    fun STATE tacfun st = tacfun st st;
+* HOLCF: fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
 
-* 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;
+* added extended adm_tac to simplifier in HOLCF.  Can now discharge
+  adm (%x. P (t x)), where P is chainfinite and t continuous.