*** empty log message ***
authornipkow
Thu Oct 30 09:54:47 1997 +0100 (1997-10-30)
changeset 40356ffbc7b11abd
parent 4034 5bb30bedbdc2
child 4036 bd686e39bff8
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Thu Oct 30 09:47:26 1997 +0100
     1.2 +++ b/NEWS	Thu Oct 30 09:54:47 1997 +0100
     1.3 @@ -80,11 +80,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of
     1.8 -Actions;
     1.9 +* HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
    1.10  
    1.11  * HOL/Auth: new protocol proofs including some for the Internet
    1.12 -protocol TLS;
    1.13 +  protocol TLS;
    1.14  
    1.15  * HOL/Map: new theory of `maps' a la VDM.
    1.16  
    1.17 @@ -95,10 +94,25 @@
    1.18  * HOL/simplifier: terms of the form
    1.19    `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)
    1.20    are rewritten to
    1.21 -  `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)'
    1.22 +  `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',
    1.23 +  and those of the form
    1.24 +  `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)' (or t=x)
    1.25 +  are rewritten to
    1.26 +  `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',
    1.27 +
    1.28 +* HOL/datatype
    1.29 +  Each datatype `t' now comes with a theorem `split_t_case' of the form
    1.30  
    1.31 -* HOL/Lists: the function "set_of_list" has been renamed "set" (and
    1.32 -its theorems too);
    1.33 +  P(t_case f1 ... fn x) =
    1.34 +     ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
    1.35 +        ...
    1.36 +        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
    1.37 +     )
    1.38 +
    1.39 +  which can be added to a simpset via `addsplits'.
    1.40 +
    1.41 +* HOL/Lists: the function "set_of_list" has been renamed "set"
    1.42 +  (and its theorems too);
    1.43  
    1.44  
    1.45  *** HOLCF ***