NEWS
changeset 14333 14f29eb097a3
parent 14285 92ed032e83a1
child 14361 ad2f5da643b4
equal deleted inserted replaced
14332:fd3535af90ab 14333:14f29eb097a3
    21 
    21 
    22 * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 
    22 * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 
    23   allowed in identifiers. Similar to greek letters \<^isub> is now considered 
    23   allowed in identifiers. Similar to greek letters \<^isub> is now considered 
    24   a normal (but invisible) letter. For multiple letter subscripts repeat 
    24   a normal (but invisible) letter. For multiple letter subscripts repeat 
    25   \<^isub> like this: x\<^isub>1\<^isub>2. 
    25   \<^isub> like this: x\<^isub>1\<^isub>2. 
       
    26 
       
    27 * Pure: There are now sub-/superscripts that can span more than one
       
    28   character. Text between \<^bsub> and \<^esub> is set in subscript in
       
    29   PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The
       
    30   new control characters are not identifier parts.
    26 
    31 
    27 * Pure: Using new Isar command "finalconsts" (or the ML functions
    32 * Pure: Using new Isar command "finalconsts" (or the ML functions
    28   Theory.add_finals or Theory.add_finals_i) it is now possible to
    33   Theory.add_finals or Theory.add_finals_i) it is now possible to
    29   declare constants "final", which prevents their being given a definition
    34   declare constants "final", which prevents their being given a definition
    30   later.  It is useful for constants whose behaviour is fixed axiomatically
    35   later.  It is useful for constants whose behaviour is fixed axiomatically