Re: [isabelle] Accessing ML terms in Isabelle theory



Dear Iulia,

> I would like to ask if and how it is possible to refer in an Isabelle
> theory to an ML defined term. For example, I have the following theory:

there has been a thread on this mailing list recently:


<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-June/msg00076.html>

The bottom line is: It's possible; but to make it work correctly, some
more thought is required. You can find an early prototype here:

  <https://github.com/larsrh/purely-experimental>

Have a look at the file "Splice_Examples.thy".

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.