I quite often find that I want to use a new character in
ProofPower HOL.

However, ProofPower seems to be quite fussy about what
characters you use.

For example, there are three "spares" at the moment,
which would be useful for me. They wouldn't look right
in xpp but I could get them to print nicely.
However, ProofPower rejects the use of these characters.

Also, some of the characters which are not "spare" and
are in the palette are rejected altogether, e.g. the
equivalence symbol (three horizontal bars).

Would there be any problem in extending the set of
of characters which are accepted in HOL terms?

Roger Jones

Proofpower mailing list

Reply via email to