tuned;
authorwenzelm
Sat May 01 22:28:51 2004 +0200 (2004-05-01)
changeset 146992c9b463044ec
parent 14698 7e4dec3fd515
child 14700 2f885b7e5ba7
tuned;
NEWS
     1.1 --- a/NEWS	Sat May 01 22:27:25 2004 +0200
     1.2 +++ b/NEWS	Sat May 01 22:28:51 2004 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  parsing/printing, see also isar-ref manual.
     1.5  
     1.6  * Pure: improved indexed syntax and implicit structures.  First of
     1.7 -call, indexed syntax provides a notational device for subscripted
     1.8 +all, indexed syntax provides a notational device for subscripted
     1.9  application, using the new syntax \<^bsub>term\<^esub> for arbitrary
    1.10  expressions.  Secondly, in a local context with structure
    1.11  declarations, number indexes \<^sub>n or the empty index (default