Make S usable as a variable by hiding the S constant from combinTheory
Many tweaks and fixups, mostly to HOL notation-ish stuff.

Some wording changes also.
Add .gitignore to ignore itp2014.ps