For this one I'm not sure if we finalised a markup form that distinguished the
different semantic parts of proofstate output, although it was certainly
discussed and seems useful. The Eclipse interface uses an xslt style sheet to
render to an HTML widget, so you could add your own tags and inte
In sort of the same vein, in Coq, we have named hypotheses in our
proof contexts which render like:
Hyp0 : Hyp (P x)
Hyp1 : Hyp (P z)
or (P x) (or (forall y : U, P y) False)
I'd like to add some PGML so that it looks something like this:
Hyp0 :
