* 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
