[opentheory-users] Isabelle

[Ramana Kumar]

How much (and what) work would be necessary to extend OpenTheory
interoperability to Isabelle/HOL?
Is that a long-term goal of the project?
What about to non-HOL provers? I certainly imagine ideas from
OpenTheory might be used in an even more radical inter-logic theory
packaging system, but could that system in fact be a distant version
of OpenTheory itself?