Define entrypoint to change grammars to be tight/loose equality

Existing entrypoints change the global grammar; new functions make it
easy to adjust arbitrary grammar values.

Restore ppstream_funs as nullary type operator in term_pp_types

This name is used in user-written code (users' special purpose
pretty-printers), and there is no reason to rebind this name, forcing
them to change things.

Up to hol.state0

Preserve add_user_printer properly in grammar data

This requires a slightly involved process for storing references to
code in theory files.

Update the .doc file on add_user_printer (which was already incredibly
long), and add a test.

Closes #367

User pp fns can note terms as binders to system printer

This allows better behaviour in a test case shown to me by Mike, where
annotations in monad-syntax weren't appearing.

Allow case-constant printing to be overridden by user overloads.

For the if-then-else case, the specially installed user-printer code
from ParseExtras needs to be adjusted.

Closes #206

Provide more options for futzing with ='s precedence

Now there are four functions:

{temp,}_{tight,loose}_equality

The temp versions create an effect that is not exported in the theory
file, and can be called before new_theory without causing annoying
error messages about changes being discarded.

The tight precedence is 450, which is the same level as the other
standard relational operators (e.g., <). The loose precedence is 100,
which is historical, and clearly appropriate for = construed as iff.

Improve pretty-printing of if-then-else. Closes #20

Include some regression tests.

Change src/bool to src/1 as a prelude to experimentation!