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, forever.

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 to ask.

Regards,
GB





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