Misc

[benjub]

Several typos, but also, in my mathbox, an axiom with $d ph ps $. in order to see if mmj2 complains, following the discussion on the discussion group with @digama0

I'll see whether it complains or not, but I should probably comment it out in any case.

[nmegill]

This is interesting, but as mentioned in my Google Groups post I would prefer that the $d ph ps $. section be commented out for the time being. If you can do that, then I will merge this.

[benjub]

Commented out, so it's ready to merge.