Re: [ProofPower] Extended character support
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
Re: [ProofPower] Extended character support
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
Re: [ProofPower] Extended character support
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
[ProofPower] Extended character support
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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
