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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and