Hi David et al.,
I'm running the Isabelle theorem prover on top of Poly/ML on a Mac OS
X PowerBook G4. I would like to be able to
1. Call Isabelle's ML functions directly from external processes that
have been written in C.
2. Call C code I've loaded into Isabelle's process space, and have
that code call back to Poly/ML functions.
Is it possible to do either of these in Poly/ML?
Thanks in advance,
-john
