Re: [isabelle] A few questions about Isabelle2013
On 1/15/2013 6:03 AM, Makarius wrote:
On Sat, 12 Jan 2013, Gottfried Barrow wrote:
\<^SUB> IS STILL THERE. IS IT STAYING THERE?
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.
I'm not really asking for any changes or new features, I'm asking, in a
roundabout way, that you leave those four commands the way they are,
I could be asking for even less, merely to know what the future holds.
If you said, "The four will eventually be reduced down to two commands",
I would say to myself, "Ah, it was a nice thought that things would stay
the same, but at least I know the future."
I can see the need to reduce those four, as they're named, down to only
two commands, but that the executive decision might need some more time
to be thought out or to implement.
But, commands like \<^isub>\<lfloor> and \<^isub>\<rfloor> would make
good markup commands. I can't use those particular two because I might
use the floor function in the index of a sigma sum, not that I've
completely thought that out.
There are plenty of other characters to choose from, but in these
formative stages, when things haven't been set in stone, it doesn't hurt
This archive was generated by a fusion of
Pipermail (Mailman edition) and