HoTT/HoTT — pull request #179 by JasonGross (2013-08-15 18:57:25+00:00)
Title: Comment out the symmetry tactic notation

It doesn't actually work, so it's best to not confuse people. Instead,
I've added a comment about what we'd like to do.