HoTT/HoTT — pull request #132 by JasonGross (2013-07-01 17:46:40+00:00)
Title: Change a Notation into an alias

It doesn't need to be a keyword, and this lets us redefine "unit_name",
should we ever want to.

(If you want, I can get rid of the remove-the-trailing-space change; emacs just does that for me automatically.)