Re: [isabelle] Isar feature request: bbold and ebold



On 9/12/2012 2:43 PM, Makarius wrote:
So in that case, I appeal to formal use only, such as \<^ibold> to signify that a variable is a vector. We all know how we'd be in a world of hurt without vectors, and how a vector is represented either with an overhead arrow, or with bold.

This can be done just with \<^bold> -- after the next reform of special identifier notation. (Although Proof General users will complain, because \<^bold> has never worked there on the display.)

Thanks. Did I not say, "Makarius has probably already thought about all of this"?

BTW, old-fashioned continental European vectors would be written in Fraktur 𝔵𝔶𝔷which is already there, but that is a bit difficult to read even for Germans.
Being mono-lingual, to compensate, it is important that Americans be well-versed in European trivia.

I reduce my requests. The commands \<^iitalic> and \<^ibold>, that's all I'm asking for now. I address the italic issue in the other reply.

So what is your application for \<^italic> in identifiers?

You may have read my other email by now, but I make my argument again.

It's purely to have another option for me to mark up a THY so that it's more readable for me. I spin here the "educational use of Isabelle like that of Mathematica". When THYs can be marked up to be very readable in their own right, then there's the possibility of passing around THY files in an educational setting, although that's not the purpose of my request.

I just want to be able to read the mathematics that I'm writing in jEdit, without having to resort to LaTeX. At a certain point, the technical hassles can kill your inspiration.

I don't know how important it would be for me to italicize variables so that they have a traditional look in jEdit. If all you have to do is add \<iitalic> in the identifier specification and in one ML file, it's my opinion that wouldn't be an unacceptable expansion of Isar, but that's me, and you didn't ask my opinion.

Regards,
GB







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