NuPRL and Isabelle are two general purpose theorem provers. Both of them are based on a version of Constructive Higher Order Type Theory. In an earlier work the author has proposed an informal semantics of Isabelle Meta Logic in an extension of NuPRL Type Theory. An automated converter, based on this semantics, has been developed, that translates Isabelle theorem statements into NuPRL. This work presents a formalization of the above semantics in NuPRL. It starts with a deep embedding of Isabelle type and term syntax into NuPRL Constructive Type Theory. Next, two internal NuPRL functions are defined. One of them maps Isabelle types into NuPRL types and the other maps Isabelle terms into elements of appropriate NuPRL types. These two functions provide an interpretation of Isabelle in NuPRL. Finally, interpretations of all Isabelle Meta Logic rules are proven as theorems in some classical extension of NuPRL Type Theory. This formalization is aimed to provide a more secure foundation for the interaction between two systems.