[ProofPower] PP and XML

[Rob Arthan]

On Thursday 26 Jan 2006 8:45 am, Roger Bishop Jones wrote:
> On Wednesday 25 January 2006 16:33, Gregg Reynolds wrote:
>...
>
> Thanks for all the stuff about emacs.
>...

A few things that may be of interest to you and Gregg, in this connection:

Proof General is implemented in emacs and uses something called X-symbol to 
display mathematical fonts. Follow links from  David Aspinall's homepage 
http://homepages.inf.ed.ac.uk/da for info on Proof General and subsequent 
developments. There is also some work on XML based mark-ups and protocols 
(PGIP) for the prover-user interface dialogue, e.g., see the various recent 
papers by David, Christopher Lueth and others.

Philip Hallam-Baker has done work on Z in HTML, see 
http://vl.zuser.org/html-z.html.

Richard Jones has design TrueType fonts for Z. See 
http://www.cs.ukc.ac.uk/people/staff/rej/Zedfont/latest/

Regards,

Rob.