[isabelle-dev] NEWS: Simplified subscripts within identifiers

Makarius makarius at sketis.net
Tue Aug 13 20:54:09 CEST 2013

* 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

* Document antiquotations: term style "isub" has been renamed to

This refers to Isabelle/a1119cf551e8, Isabelle/d0fa3f446b9d and 

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.)


More information about the isabelle-dev mailing list