Dear All,

Acting on some very helpful comments from Phil Clayton, I have revised the 
proposed scheme for translating between Unicode and the ProofPower extended 
character set. The revised scheme is described here:

(You can find the earlier version at

The new scheme for you to look at with your e-mail client follows below.

As before, Mac OS X supports all the necessary glyphs. If you install the STIX 
fonts on Linux (stix-fonts on Fedora, fonts-stix on Ubuntu), there is now a 
good chance that you will have all you need.

Any feedback will be much appreciated.



0x80: %subset%: โŠ†
0x81: %rsub%: โฉฅ
0x82: %bagunion%: โจ„
0x83: %bbU%: ๐•Œ
0x84: %Delta%: ๐›ฅ
0x85: %fcomp%: โˆ˜
0x86: %Phi%: ๐›ท
0x87: %Gamma%: ๐›ค
0x88: %EZ%: โ””
0x89: %down%: โ‹Ž
0x8A: %Theta%: ๐›ฉ
0x8B: %dcat%: โ€/
0x8C: %Lambda%: ๐›ฌ
0x8D: %mem%: โˆˆ
0x8E: %notmem%: โˆ‰
0x8F: %bij%: โค–
0x90: %Pi%: ๐›ฑ
0x91: %SML%: โ“œ
0x92: %rres%: โ–ท
0x93: %Sigma%: ๐›ด
0x94: %<:%: โ“ฃ
0x95: %Upsilon%: ๐›ถ
0x96: %boolean%: ๐”น
0x97: %Omega%: ๐›บ
0x98: %Xi%: ๐›ฏ
0x99: %Psi%: ๐›น
0x9A: %emptyset%: โˆ…
0x9B: %up%: โ‹
0x9C: %BHH%: โ•
0x9D: %SZG%: โ•’
0x9E: %finj%: โค•
0x9F: %ffun%: โ‡ป
0xA0: %psubset%: โŠ‚
0xA1: %intersect%: โˆฉ
0xA2: %rseq%: โŸฉ
0xA3: %symdiff%: โŠ–
0xA4: %equiv%: โ‡”
0xA5: %dintersect%: โ‹‚
0xA6: %def%: โ‰œ
0xA7: %lseq%: โŸจ
0xA8: %lrelimg%: โฆ‡
0xA9: %rrelimg%: โฆˆ
0xAA: %rel%: โ†”
0xAB: %overwrite%: โŠ•
0xAC: %<%: โŒœ
0xAD: %fun%: โ†’
0xAE: %>%: โŒ
0xAF: %real%: โ„
0xB0: %EFT%: โ– 
0xB1: %and%: โˆง
0xB2: %or%: โˆจ
0xB3: %not%: ยฌ
0xB4: %implies%: โ‡’
0xB5: %forall%: โˆ€
0xB6: %exists%: โˆƒ
0xB7: %spot%: โฆ
0xB8: %x%: ร—
0xB9: %SFT%: โ“ˆ
0xBA: %bigcolon%: โฆ‚
0xBB: %rcomp%: โจพ
0xBC: %leq%: โ‰ค
0xBD: %neq%: โ‰ 
0xBE: %geq%: โ‰ฅ
0xBF: %symbol%: ๐•Š
0xC0: %union%: โˆช
0xC1: %alpha%: ๐›ผ
0xC2: %beta%: ๐›ฝ
0xC3: %refinedby%: โŠ‘
0xC4: %delta%: ๐›ฟ
0xC5: %select%: ๐œ€
0xC6: %phi%: ๐œ‘
0xC7: %gamma%: ๐›พ
0xC8: %eta%: ๐œ‚
0xC9: %iota%: ๐œ„
0xCA: %theta%: ๐œƒ
0xCB: %kappa%: ๐œ…
0xCC: %fn%: ๐œ†
0xCD: %mu%: ๐œ‡
0xCE: %nu%: ๐œˆ
0xCF: %psurj%: โค€
0xD0: %pi%: ๐œ‹
0xD1: %chi%: ๐œ’
0xD2: %rho%: ๐œŒ
0xD3: %sigma%: ๐œŽ
0xD4: %tau%: ๐œ
0xD5: %upsilon%: ๐œ
0xD6: %complex%: โ„‚
0xD7: %omega%: ๐œ”
0xD8: %xi%: ๐œ‰
0xD9: %psi%: ๐œ“
0xDA: %zeta%: ๐œ
0xDB: %SX%: โฆ
0xDC: %BV%: โ”‚
0xDD: %EX%: โฆŽ
0xDE: %dunion%: โ‹ƒ
0xDF: %pfun%: โ‡ธ
0xE0: %inj%: โ†ฃ
0xE1: %dsub%: โฉค
0xE2: %bottom%: โŠฅ
0xE3: %Leftarrow%: โ‡
0xE4: %psupset%: โŠƒ
0xE5: %supset%: โŠ‡
0xE6: %fset%: ๐”ฝ
0xE7: %uptext%: โ†—
0xE8: %dntext%: โ†˜
0xE9: %replacedby%: โ‰ก
0xEA: %cantext%: โ†•
0xEB: %cat%: โ€
0xEC: %extract%: โ†ฟ
0xED: %map%: โ†ฆ
0xEE: %nat%: โ„•
0xEF: %surj%: โ† 
0xF0: %pset%: โ„™
0xF1: %SZT%: โ“ฉ
0xF2: %dres%: โ—
0xF3: %rat%: โ„š
0xF4: %thm%: โŠข
0xF5: %ulbegin%: โจฝ
0xF6: %ulend%: โจผ
0xF7: %BT%: โ”œ
0xF8: %uminus%: ๏นฃ
0xF9: %filter%: โ†พ
0xFA: %int%: โ„ค
0xFB: %lbag%: โŸฆ
0xFC: %BH%: โ”€
0xFD: %rbag%: โŸง
0xFE: %pinj%: โค”
0xFF: %SZS%: โ”Œ

Proofpower mailing list

Reply via email to