Add fuller affiliation and ARC acknowledgment.
Explain universal set notation.
Use sans serif constants.
textsf constants look better if they’re a bit smaller.
oleast in binder-mode doesn’t get the desired \HOLConst wrapper.

This is almost certainly a bug in the HOL pretty-printer, but it’s
easy enough to handle with overrides in this one case.
Typeset a theorem a bit better.