[Iris-Club] ∗ for separating conjunction
mail at robbertkrebbers.nl
Tue Nov 1 14:55:40 CET 2016
Dave Swasey recommended to use the symbol ∗ for separating conjunction
(instead of the current ★) because it looks nicer and better matches
conventional practice. I have created a merge request, see:
Please let me know ASAP (∗) if you are opposed, for example, because you
cannot distinguish ∗ and * in your favorite font.
(∗) If we perform this change, I would like to use the new symbol in the
proof mode paper, whose camera ready version is due Monday.
More information about the Iris-Club