# HG changeset patch
# User wenzelm
# Date 1010952763 -3600
# Node ID 80f10551fb5941006e1a36407799cef61d0ac165
# Parent  09a224f7d77648e701be8b67834583cd189682dc
* HOL: symbolic syntax for x^2 (numeral 2);

diff -r 09a224f7d776 -r 80f10551fb59 NEWS
--- 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