[isabelle-dev] NEWS: Simplified subscripts within identifiers

[Makarius]

* Simplified subscripts within identifiers, using plain \<^sub>
instead of the second copy \<^isub> and \<^isup>.  Superscripts are
only for literal tokens within notation; explicit mixfix annotations
for consts or fixed variables may be used as fall-back for unusual
names.  Obsolete \<twosuperior> has been expanded to \<^sup>2 in
Isabelle/HOL.  INCOMPATIBILITY, use "isabelle update_sub_sup" to
standardize symbols as a starting point for further manual cleanup.
The ML reference variable "legacy_isub_isup" may be set as temporary
workaround, to make the prover accept a subset of the old identifier
syntax.

* Document antiquotations: term style "isub" has been renamed to
"sub".  Minor INCOMPATIBILITY.


This refers to Isabelle/a1119cf551e8, Isabelle/d0fa3f446b9d and 
AFP/f5d0bafd208b.

The simplification also means that some key sequences for subscripts in 
Isabelle/jEdit have changed.  People connected to the repository need to 
ensure that $ISABELLE_HOME_USER/jedit/keymaps/ is refreshed.  An easy way 
is to delete that directory -- jEdit will recreate it from the default 
properties that the Isabelle/jEdit distribution provides.  (This will 
purge any personal keyboard shortcuts.)


 	Makarius