Add to ORKGInternational audienceWe show how modern proof environments comprising code generators andreflection facilities can be used for the effective construction of atool for OCL. For this end, we define a UML/OCL meta-model in HOL, ameta-model for Isabelle/HOL in HOL, and a compiling function betweenthem over the vocabulary of the libraries provided by FeatherweightOCL. We use the code generator of Isabelle to generate executable codefor the compiler, which is bound to a USE tool-like syntax integratedin Isabelle/Featherweight OCL. It generates for an arbitrary classmodel an object-oriented datatype theory and proves the relevantproperties for casts, type-tests, constructors and selectorsautomatically