changeset 53016 fa9c38891cf2
parent 52949 90edb0669845
child 53021 d0fa3f446b9d
--- a/NEWS	Tue Aug 13 16:25:47 2013 +0200
+++ b/NEWS	Tue Aug 13 17:26:22 2013 +0200
@@ -6,6 +6,17 @@
 *** General ***
+* 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
 * Uniform management of "quick_and_dirty" as system option (see also
 "isabelle options"), configuration option within the context (see also
 Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor