[isabelle] ML vs XML vs YXML
Several people have asked about it, so here it is: an OCaml version of the
ML value representation in XML, and the YXML transfer syntax. See
https://bitbucket.org/makarius/yxml (changeset 146b7018ad02 right now).
The README also contains an example with some Isabelle/HOL term in yxml
format that can be loaded into OCaml.
The general principle might turn out useful to transfer types, terms,
proofs etc. between Isabelle and Coq, HOL-Light, HOL0 etc. Maybe the
HOL-Light-Import renovation project can use it already.
Basically, this stuff should scale to some extent, but I have no
experience with constraints imposed by the OCaml runtime system (which
generally feels a bit old-fashioned).
This archive was generated by a fusion of
Pipermail (Mailman edition) and