Dear Makarius,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? I use the diamond symbol a lot (for applicative functor syntax) and I found the smaller symbol much less invasive. (I feel it is also closer to the standard \diamond symbol in LaTeX.) I've attached a screenshot with both versions of Isabelle. (Ubuntu Linux 14.04, jEdit text font is IsabelleText at size 14).
Description: PNG image