Automatic translation from Isabelle/HOL to HOL

Question

I have some definitions and theorems in Isabelle/HOL and need to use those same definitions and theorems with HOL. Translating the code manually is certainly possible, but cumbersome. Are there any programs that (semi-)automatically perform such a translation?

If this is not possible for some reason, please explain why, since this would be an important learning for me.

Answer 1

In theory, you should be able to easily move theorems and definitions between HOL implementations, and this idea is the motivation of the OpenTheory project. Unfortunately, in practice, Isabelle's implementation of HOL is sufficiently different from the others, and per the OpenTheory page Isabelle only has the ability to import theorems using OpenTheory, and cannot export them, at present.