HoTT/HoTT — pull request #376 by JasonGross (2014-04-21 21:38:33+00:00)
Title: Utf8 notations

This replaces part 2 of #373, and is on top of #375.

This gives a file that can be imported to display unicode notations.