# HG changeset patch
# User nipkow
# Date 878201687 -3600
# Node ID 6ffbc7b11abd096c52ce5aed1fc96ad494c0308b
# Parent  5bb30bedbdc291673cadf1caff71a7f6653aeb2f
*** empty log message ***

diff -r 5bb30bedbdc2 -r 6ffbc7b11abd NEWS
--- a/NEWS	Thu Oct 30 09:47:26 1997 +0100
+++ b/NEWS	Thu Oct 30 09:54:47 1997 +0100
@@ -80,11 +80,10 @@
 
 *** HOL ***
 
-* HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of
-Actions;
+* HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
 
 * HOL/Auth: new protocol proofs including some for the Internet
-protocol TLS;
+  protocol TLS;
 
 * HOL/Map: new theory of `maps' a la VDM.
 
@@ -95,10 +94,25 @@
 * HOL/simplifier: terms of the form
   `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)
   are rewritten to
-  `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)'
+  `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',
+  and those of the form
+  `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)' (or t=x)
+  are rewritten to
+  `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',
+
+* HOL/datatype
+  Each datatype `t' now comes with a theorem `split_t_case' of the form
 
-* HOL/Lists: the function "set_of_list" has been renamed "set" (and
-its theorems too);
+  P(t_case f1 ... fn x) =
+     ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
+        ...
+        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
+     )
+
+  which can be added to a simpset via `addsplits'.
+
+* HOL/Lists: the function "set_of_list" has been renamed "set"
+  (and its theorems too);
 
 
 *** HOLCF ***