Re: [isabelle] Isabelle2016-RC0: font size of diamond symbol
On Fri, 8 Jan 2016, Andreas Lochbihler wrote:
While trying out Isabelle2016-RC0, I noticed that the symbol for
\<diamond> is now typeset much larger than in Isabelle2015. Has this
change been intentional?
date: Thu Dec 31 12:20:10 2015 +0100
files: lib/fonts/IsabelleText.sfd lib/fonts/IsabelleTextBold.sfd
proper diamond from lasy10;
"Proper" means the rendering of \<diamond> corresponds to \<box>, for
typical use in temporal logics. The traditional situation in
lib/texinputs/isabellesym.sty and its group "logic" in etc/symbols
supports this interpretation.
I use the diamond symbol a lot (for applicative functor syntax) and I
found the smaller symbol much less invasive.
There is a small diamond in the IsabelleText font as well. Historically
it was assigned to \<struct> but that has lost its purpose. So in
Isabelle/0046bacc5f5b, I have now added a newly interpreted symbol
\<diamondop> to use that glyph.
The very few applications that did use \<diamond> as infix operator are
already updated, notably in AFP/363fdbc2f28c.
This archive was generated by a fusion of
Pipermail (Mailman edition) and