Re: [isabelle] A few questions about Isabelle2013



On Sat, 12 Jan 2013, Gottfried Barrow wrote:

\<^SUB> IS STILL THERE. IS IT STAYING THERE?

In Isabelle 2013, nothing has changed in regards to \<^isub>, \<^isup>, \<^sub>, and \<^sup>. Are \<^sub> and \<^sup> (or something equivalent) going to stay in Isar forever, or are they going away? If they're not going away, I'll use them exclusively for the markup I talked about previously. If they're going away, I won't use them at all.

The problem is not \<^sub> and \<^sup>, but the second copy \<^isub> and \<^isup> for identifier syntax. This is an old issue stemming from 2003, when that feature was introduced. Back then there were reasons to do it like that, and *after* the coming release one might considere re-opening the can to sort it out.

At the moment there are far more pressing things, notably getting Isabelle2013 in a stable state, not putting more changes and features in at this point.


	Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.