[Iris-Club] ∗ for separating conjunction

Robbert Krebbers mail at robbertkrebbers.nl
Tue Nov 1 14:55:40 CET 2016

Hi all,

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 mailing list