*** empty log message ***
authornipkow
Fri Oct 16 08:48:05 1998 +0200 (1998-10-16)
changeset 5651ca45d6126c8a
parent 5650 38bda28c68a2
child 5652 fe5f5510aef4
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Thu Oct 15 12:15:14 1998 +0200
     1.2 +++ b/NEWS	Fri Oct 16 08:48:05 1998 +0200
     1.3 @@ -254,11 +254,17 @@
     1.4  * HOL/Relation: renamed the relational operator r^-1 "converse"
     1.5  instead of "inverse";
     1.6  
     1.7 +* HOL/Induct/Multiset: a theory of multisets, including the wellfoundedness
     1.8 +  of the multiset ordering;
     1.9 +
    1.10  * directory HOL/Real: a construction of the reals using Dedekind cuts
    1.11 -(not included by default);
    1.12 +  (not included by default);
    1.13  
    1.14  * directory HOL/UNITY: Chandy and Misra's UNITY formalism;
    1.15  
    1.16 +* directory HOL/Hoare: a new version of Hoare logic which permits many-sorted
    1.17 +  programs, i.e. different program variables may have different types.
    1.18 +
    1.19  * calling (stac rew i) now fails if "rew" has no effect on the goal
    1.20    [previously, this check worked only if the rewrite rule was unconditional]
    1.21    Now rew can involve either definitions or equalities (either == or =).