1.1 --- a/NEWS	Tue Aug 13 16:25:47 2013 +0200
     1.2 +++ b/NEWS	Tue Aug 13 17:26:22 2013 +0200
     1.3 @@ -6,6 +6,17 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Simplified subscripts within identifiers, using plain \<^sub>
     1.8 +instead of the second copy \<^isub> and \<^isup>.  Superscripts are
     1.9 +only for literal tokens within notation; explicit mixfix annotations
    1.10 +for consts or fixed variables may be used as fall-back for unusual
    1.11 +names.  Obsolete \<twosuperior> has been expanded to \<^sup>2 in
    1.12 +Isabelle/HOL.  INCOMPATIBILITY, use "isabelle update_sub_sup" to
    1.13 +standardize symbols as a starting point for further manual cleanup.
    1.14 +The ML reference variable "legacy_isub_isup" may be set as temporary
    1.15 +workaround, to make the prover accept a subset of the old identifier
    1.16 +syntax.
    1.17 +
    1.18  * Uniform management of "quick_and_dirty" as system option (see also
    1.19  "isabelle options"), configuration option within the context (see also
    1.20  Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor