On Mon, 9 Apr 2012, Edward Z. Yang wrote:
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.
Maybe I've misunderstood this as a misunderstanding. The example term
representation for the YXML library is exactly the Isabelle term datatype.
But that is really just an example, it is not really useful for the
problem to connect users to proof checkers.
Makarius
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
