# HG changeset patch
# User nipkow
# Date 908520485 -7200
# Node ID ca45d6126c8a527e81f573220f3b8f74e273b708
# Parent  38bda28c68a21022cb471bd2d529029e78cc1a8a
*** empty log message ***

diff -r 38bda28c68a2 -r ca45d6126c8a NEWS
--- a/NEWS	Thu Oct 15 12:15:14 1998 +0200
+++ b/NEWS	Fri Oct 16 08:48:05 1998 +0200
@@ -254,11 +254,17 @@
 * HOL/Relation: renamed the relational operator r^-1 "converse"
 instead of "inverse";
 
+* HOL/Induct/Multiset: a theory of multisets, including the wellfoundedness
+  of the multiset ordering;
+
 * directory HOL/Real: a construction of the reals using Dedekind cuts
-(not included by default);
+  (not included by default);
 
 * directory HOL/UNITY: Chandy and Misra's UNITY formalism;
 
+* directory HOL/Hoare: a new version of Hoare logic which permits many-sorted
+  programs, i.e. different program variables may have different types.
+
 * calling (stac rew i) now fails if "rew" has no effect on the goal
   [previously, this check worked only if the rewrite rule was unconditional]
   Now rew can involve either definitions or equalities (either == or =).