On 5 Jun 2009, at 08:35, Roger Bishop Jones wrote:

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.

Yes - you can add entries for additional symbols in the sievekeyword files so that doctex understands them.


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).

Aside: you can customise the palette, e.g., to add in the three spares. Have a look at app-defaults/Xpp.


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

No. You can do it yourself:

val _ =
        let     open  ReaderWriterSupport.PrettyNames;
        in      add_new_symbols [ (["identeq"], Value "\233", Simple) ]
        end;

After that you can use the three-barred gate or equivalently %identeq% in HOL types and terms.

You can use the character from the xpp palette instead of \233 in the above if you like.

Even when you run out of extended characters, you can use Nil to add new symbols that only have the %XXX% form.

Regards,


Rob.



_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to