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

Reply via email to