HOL: eliminated global items;

--- a/NEWS	Thu Sep 27 22:29:57 2001 +0200
+++ b/NEWS	Thu Sep 27 22:30:09 2001 +0200
@@ -43,6 +43,12 @@
 * HOL/GroupTheory: group theory examples including Sylow's theorem, by
 Florian Kammüller;
 
+* HOL: eliminated global items
+
+  const "()" -> "Product_Type.Unity"
+  type "unit" -> "Product_Type.unit"
+
+
 
 *** ZF ***