Isabelle and NuPRL are two theorem proving environments that are written in different dialects of ML using different formula syntaxes and different logical foundations. In spite of this, they have similar sets of basic theories, representing the same mathematical concepts. This paper presents the design of an automated converter from Isabelle into NuPRL that allows sharing formal knowledge between these two provers. Such sharing eliminates the need for re-proving the same results in different systems and opens door for joint work on large verification projects. The paper starts with an overview of the problem and of the related works. The second part outlines the embedding of Isabelle syntax into NuPRL and technical details of the converter design. In the third section logical soundness of this embedding is shown.