Re: [isabelle] Running opentheory in Isabelle



For posterity:

> When I load the so-generated theory file, I can't access the hidden
> "PolyML" structure.

The only required operation from "PolyML" is "pointerEq":

SML_import \<open>structure PolyML = struct val pointerEq = pointer_eq
end;\<close>

With that prefixed before loading the other files, it works. Makarius
figured this out.




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