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