NEWS
changeset 14699 2c9b463044ec
parent 14698 7e4dec3fd515
child 14700 2f885b7e5ba7
equal deleted inserted replaced
14698:7e4dec3fd515 14699:2c9b463044ec
    18 * Pure: 'advanced' translation functions (parse_translation etc.) may
    18 * Pure: 'advanced' translation functions (parse_translation etc.) may
    19 depend on the signature of the theory context being presently used for
    19 depend on the signature of the theory context being presently used for
    20 parsing/printing, see also isar-ref manual.
    20 parsing/printing, see also isar-ref manual.
    21 
    21 
    22 * Pure: improved indexed syntax and implicit structures.  First of
    22 * Pure: improved indexed syntax and implicit structures.  First of
    23 call, indexed syntax provides a notational device for subscripted
    23 all, indexed syntax provides a notational device for subscripted
    24 application, using the new syntax \<^bsub>term\<^esub> for arbitrary
    24 application, using the new syntax \<^bsub>term\<^esub> for arbitrary
    25 expressions.  Secondly, in a local context with structure
    25 expressions.  Secondly, in a local context with structure
    26 declarations, number indexes \<^sub>n or the empty index (default
    26 declarations, number indexes \<^sub>n or the empty index (default
    27 number 1) refer to a certain fixed variable implicitly.  Typical
    27 number 1) refer to a certain fixed variable implicitly.  Typical
    28 applications of these concepts involve record types and locales.
    28 applications of these concepts involve record types and locales.