# HG changeset patch
# User nipkow
# Date 877683921 -7200
# Node ID 2a903ba8d39e7222f516e45925533e9a0f5374a4
# Parent  b4f93a8da8359181d0fa5245a7e86adc8062000b
HOL/Map

diff -r b4f93a8da835 -r 2a903ba8d39e NEWS
--- a/NEWS	Fri Oct 24 10:31:31 1997 +0200
+++ b/NEWS	Fri Oct 24 11:05:21 1997 +0200
@@ -80,6 +80,8 @@
 
 *** HOL ***
 
+* HOL/Map: new theory of `maps' a la VDM.
+
 * HOL/simplifier: added infix function `addsplits':
   instead of `<simpset> setloop (split_tac <thms>)'
   you can simply write `<simpset> addsplits <thms>'