Re: [isabelle] 5 proofs of concept satisfied and awesomeness revisited
On Thu, 12 Jul 2012, Gottfried Barrow wrote:
(3) Can the syntax of Isabelle be made to look very, very mathematical?
I already knew about the available math symbols, and the structured
proofs, which was part of the initial attraction. I showed in a recent
email that Isar identifiers can be made to look mathematical. Let no man
or woman say that single, subscripted Latin, Greek, mathcal, or mathfrak
alphabet characters do not meet the requirements of looking
For those who don't know, an Isar identifier can use 0-9, ', and _,
though it can't start with those characters. In addition, it can use
a-z, A-Z, \<a> - \<z>, \<A> - \<Z>, \<aa> - \<zz>, \<AA> - \<ZZ> (but
not II and RR) , and the lower and upper case Greek alphabet, such as
\<alpha>. You can use \<^isub> and \<^isup> followed by the
aforementioned characters anywhere you want, and as many times as you
want. That's some major naming options, compared to most programming
Note that concerning the prover backend, both \<II> \<RR> *are* allowed
within identifiers; the prover gets these ASCII sequences only. You don't
see the corresponding unicode glyph in Isabelle/jEdit, though. (The
traditional dropout is \<lambda>, which is still not possible in
identifiers as \<lambda>' etc.)
The problem of \<II> and \<RR> is an overlap with the Unicode rendering of
\<Re> and \<Im>. Unlike TeX, the second copy of fraktur I and R is
missing from the Unicode 6.1 standard, cf.
This style is sometimes known as black-letter. Black-letter symbols
already encoded in the Letterlike Symbols block are omitted here to
avoid duplicate encoding."
Donald Knuth and the AMS knew better, and provided separate copies, with
slightly different shape.
Our IsabelleText font happens to have I and R glyphs in the Fraktur slot
unofficially, but I did not use them in the default mapping of
Isabelle2012/etc/symbols. Instead of stretching unicode too far, I am
considering to remove the default rendering for \<Re> and \<Im> instead,
to make the fraktur alphabet more uniform.
(And yes, Unicode is notorious to require long explanations and
considerations for seemingly trivial things.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and