A General Method for Safely Overwriting Theories in Mechanized Mathematics Systems William M. Farmer 1994 Abstract We propose a general method for overwriting theories with model conservative extensions in mechanized mathematics systems. Model conservative extensions, which include the definition of new constants and the introduction of new abstract datatypes, are ``safe'' because they preserve models as well as consistency. The method employs the notions of theory interpretation and theory instantiation. It is illustrated using many-sorted first-order logic, but it works for a variety of underlying logics.