We present the theorem proving environment holocl that is integrated in a Model-driven Engineering (mde) framework. holocl allows to reason over uml class models annotated with ocl specifications. Thus, holocl strengthens a crucial part of the uml to an object-oriented formal method. holocl provides several derived proof calculi that allow for formal derivations establishing the validity of uml/ocl formulae. These formulae arise naturally when checking the consistency of class models, when formally refining abstract models to more concrete ones or when discharging side-conditions from model-transformations.