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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
