Fix some type pretty-printing buglets

- nesting under parentheses was wrong
- type annotations (e.g., when show_types is on) were ugly

With a selftest

Fix let-p/printing to lose spaces after semicolons in binding lists

These spaces are inconsistent with the way semicolons are "spaced" in
all other contexts (monad syntax, lists, sets, function updates).

Thanks to Andreas Lööw for the bug report.

Fix bug in PAT_ASSUM when use of variables from goal is not respected

In particular, the old code gave itself licence to instantiate type
variables in patterns when those were associated with variables from
the goal, thereby allowing it to pick completely different
assumptions that didn't even include the quoted variable. The test
case illustrates.

Where a proof breaks (as in io_onestepTheory), the fix is to remove
the use of goal-variables of the wrong type, perhaps replacing them
with underscores.

Fix a resolve_then bug when the goal should be completely solved

Implement, document and regression-test some "term tactics"

Fix goalstate p/printing selftest given changes in 02199f5e5876

Fiddle with goalstate printing

Some indentation and spacing changes, but most important are:
- attach a number (0) to the assumption in goals with just one
assumption. Sometimes it is otherwise hard to parse a state and
remember which is the goal, and which is the assumption
- make "print goal at top" false by default

Test round-tripping printing+parsing (à la Pollack consistency)

Allow vars to have symbolic names without $var$(...) quoting them

Test checks that a bare > prints just as > rather than $var$(>)

Fix a bunch of breakages caused by assuming term to be an eqtype

Fix another conditional-expression p/printing oddity

The if-then- block wasn't necessarily aligned with the last else block
because the whole if-then-else wasn't guaranteed to appear in one
block to itself.

Closes #588

Also tweak error-reporting from testutils.tpp (use ␣ (U+2423) for
spaces to make spotting differences easier; control colours better).

Fix bug in generation of case_eq theorem for 'a itself

Implement Haskell-style $ as infix function application operator

With documentation and some simple test cases.

Fix a pretty-printing bug in handling let-expressions

As with 2abd7a6 and 4d125108, the issue was putting
strings (parentheses in this case) outside the Oppen-block rather than
inside it.

Make quote-filter handle newlines in type quotations consistently

As discovered by Brian Campbell (see #534), the quotation filter was
emitting a backslash escape sequence to print newlines when that
newline immediately followed the type's leading colon. Adjust this to
emit \\n\\\n\\ instead, which is what is done elsewhere in the
quotation.

Also add test-case for that parse.

Better handle Oppen-blocks under parentheses

Closes #530

Tweaks to goal pretty-printing along with tests

Fix goalstack printing bug, add regression tests

Add selftest for goal-p/printing