Uwe Brauer writes:
First an ignorant question: what is proofgeneral and how is it
to enter Xemacs?
ProofGeneral is an Emacs-based (IIRC) front-end for several proof
assistants. It would enter as a package. AFAICS, there's no
particular need for it to be restricted to XEmacs 21.5.
I am curious: for what reason do the general proof people need
which is mainly thought for latex documents and has some HTML/SGML
For the same reason that LaTeX users want them: you can get the usual
glyphs for Greek letters, logical quantifiers, and operators, instead
of using some verbose transliteration.
XEmacs-Beta mailing list