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

On Wed, 12 Sep 2012, Gottfried Barrow 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.)

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.

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?


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