Insert a missing left-paren.
Make oneTheory.one |- !v:one. v = () an automatic rewrite.

The simplifier handles this properly, and won't start rewriting ()
to itself in an infinite loop.
Allow Unicode characters to delimit various quotation forms.

Syntax highlighting might be made to work considerably better if the
beginning and end characters are different, and don't also occur as
part of a related but separate piece of syntax (quotations done with
`...`).

So, now while the old syntax is still permitted, we also allow

    ‘foo’

instead of

    `foo`

and

    “f(x+1)”

instead of

    ``f(x+1)``

The relevant characters are

    U+2018  LEFT SINGLE QUOTATION MARK
    U+2019  RIGHT SINGLE QUOTATION MARK
    U+201C  LEFT DOUBLE QUOTATION MARK
    U+201D  RIGHT DOUBLE QUOTATION MARK

This is a backwards incompatibility in that these four characters
cannot now appear as part of HOL syntax.  The fix for this might be to let
them appear in quotations where they are not being used as the delimiters.

If we implemented this more general scheme, we might also allow things
like

    U+231C  ⌜  TOP LEFT CORNER
    U+231D  ⌝  TOP RIGHT CORNER
    U+00AB  «  LEFT-POINTING DOUBLE ANGLE QUOTATION MARK
    U+00BB  »  RIGHT-POINTING DOUBLE ANGLE QUOTATION MARK

to appear as delimiters, giving more freedom to have other special
characters appear inside quotations.