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:


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:


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


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