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?

Yes, see

changeset:   62006:ebb03c0fa686
user:        wenzelm
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 MHonArc.