Dear Rob


I have just one small query - about the minus sign problem


I had a lot of trouble with this, as you might expect, when translating between 
Spivey latex and standard Z, but it can be done. I don’t know whether 
translating from Proofpower is more difficult, but it would be nice to get this 
right if possible while you are translating to Unicode. Or am I missing 


All the best





From: Proofpower [] On Behalf Of Rob 
Sent: 28 March 2015 16:03
To: ProofPower List
Subject: [ProofPower] Updated Unicode translation scheme


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