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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and