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

Huge number of check-ins, implementing change to .doc file syntax.
Now the rule for text within braces is that it appears as given, but
that braces must balance. If you want an unbalanced brace, you can use
\lbrace or \rbrace. No existing .doc file uses unbalanced braces.
Also, there is now no need to use \noindent. In fact, doing so
will get you a complaint from the parser. Similarly, use of \ or
{} characters outside of verbatim text blocks will cause griping.
All of the new files have been generated by a parse-then-print process
from the old files, and it's possible there are errors. If you ever
have a spare moment, casting your eye over a random selection of these
might help to find errors.

New versions of docfiles.