[isabelle] accessing ML definitions in isabelle_process



Hello,

I have a theory which defines

theory TestML imports Main
begin
ML
{*
    val Set_ex_bool_eq = @{thm Set.ex_bool_eq};
    val Set_all_bool_eq = @{thm Set.all_bool_eq};
*}
end

How can I access these objects from the isabelle_process?

I know that I can load the theory file using use_thy "TestML",
but I could not figure out how to access these names.

Best regards,

Viorel Preoteasa






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