[isabelle] Running opentheory in Isabelle

Dear list,

I'm currently trying to figure out whether it is feasible to provide an
opentheory interface as a "pure Isabelle theory" (in the sense that it
can be loaded in a .thy file and doesn't require an external component).

Opentheory itself builds with Poly/ML just fine.

My first approach was to take all the source files that are listed in
the Makefile and turn them into a sequence of "SML_file ..." as
indicated in the reference manual.

Unfortunately, it doesn't quite work.

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

My second approach was then to bundle everything into a "ROOT.ML" file
and load that from a theory file with "SML_file". This almost works:
When I open that "ROOT.ML" file in Isabelle/jEdit, I can see markup etc.
However, for the theory file, I get:

ML error (line 1 of "~/work/opentheory/opentheory/src/ROOT.ML"):
Value or constructor (SML_file) has not been declared

Here's the code (just the changes):


Can be cloned from the "topic/isabelle" branch of


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