[isabelle] function evaluation in ML



Hello,

I want to ask you, if there is some way to
use "value" or "normal_form" or some similar construct directly in ML{*..*}.

I just want to call function (with string result)  defined in
Isabelle/Isar from ML ,
and store that result in file..

Thanks for any suggestions.

Kamil.





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