* HOL: symbolic syntax for x^2 (numeral 2);

--- a/NEWS	Sun Jan 13 21:09:17 2002 +0100
+++ b/NEWS	Sun Jan 13 21:12:43 2002 +0100
@@ -182,6 +182,8 @@
 
   - remove all special provisions on numerals in proofs;
 
+* HOL: symbolic syntax for x^2 (numeral 2);
+
 * HOL: the class of all HOL types is now called "type" rather than
 "term"; INCOMPATIBILITY, need to adapt references to this type class
 in axclass/classes, instance/arities, and (usually rare) occurrences