Excerpts from Makarius's message of Mon Apr 09 09:50:09 -0400 2012:
> You would have compare that to the datatypes for term and proofterm in
> Isabelle, see src/Pure/term.ML and src/Pure/proofterm.ML, respectively.
Ah, so is the sample term encoding in yxml not representative of
Isabelle? I misunderstood the situation.
> If we had proper parse trees it would be easy, although having a
> fixed type of trees might be tricky with Isar's extensible parser.
In Coq, all added notations desugar to the usual parse trees. So
all I need to do is 'Set Printing All' and I get a nice, non-extended
ProofGeneral-devel mailing list