1.1 --- a/NEWS	Tue Feb 10 12:17:04 2004 +0100
     1.2 +++ b/NEWS	Wed Feb 11 00:37:18 2004 +0100
     1.3 @@ -89,7 +89,6 @@
     1.4    specification.  There is also an 'ax_specification' command that
     1.5    introduces the new constants axiomatically.
     1.6  
     1.7 -
     1.8  * arith(_tac) is now able to generate counterexamples for reals as well.
     1.9  
    1.10  * SET-Protocol: formalization and verification of the SET protocol suite;
    1.11 @@ -97,6 +96,14 @@
    1.12  * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function
    1.13   defintions, thanks to Sava Krsti\'{c} and John Matthews.
    1.14  
    1.15 +* Unions and Intersections:
    1.16 +  The x-symbol output syntax of UN and INT has been changed
    1.17 +  from "\<Union>x \<in> A. B" to "\<Union\<^bsub>x \<in> A\<^esub> B"
    1.18 +  i.e. the index formulae has become a subscript, like in normal math.
    1.19 +  Similarly for "\<Union>x. B", and for \<Inter> instead of \<Union>.
    1.20 +  The subscript version is also accepted as input syntax.
    1.21 +
    1.22 +
    1.23  New in Isabelle2003 (May 2003)
    1.24  --------------------------------
    1.25