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