Substitute implicit_rewrites for basic_rewrites in docs for Rewrite

Thanks to Piotr Trojanek for finding the problem: basic_rewrites is
now called implicit_rewrites (and is a function to boot; maybe it was
a magic value in HOL88). There isn't any documentation of
implicit_rewrites, but its nature as a function from unit is implicit
in some of the examples in the docfiles.

Closes #195
Identify some consts in non-head positions as such for pretty-printing

If an alpha-numeric identifier is the sole token in a grammar's rule,
then the pretty-printer will annotate that id as a constant.  This can
help some backends do a better job of printing.  The selftest
demonstrates this for the TeX-backend.

Closes #176