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 syntax. Edward _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
