NEWS
changeset 12736 80f10551fb59
parent 12734 c5f6d8259ecd
child 12753 3a62df7ae926
     1.1 --- a/NEWS	Sun Jan 13 21:09:17 2002 +0100
     1.2 +++ b/NEWS	Sun Jan 13 21:12:43 2002 +0100
     1.3 @@ -182,6 +182,8 @@
     1.4  
     1.5    - remove all special provisions on numerals in proofs;
     1.6  
     1.7 +* HOL: symbolic syntax for x^2 (numeral 2);
     1.8 +
     1.9  * HOL: the class of all HOL types is now called "type" rather than
    1.10  "term"; INCOMPATIBILITY, need to adapt references to this type class
    1.11  in axclass/classes, instance/arities, and (usually rare) occurrences