Definitions of new symbols merely abbreviate expressions in logical frameworks, and no new facts (regarding previously defined symbols) should hold because of a new definition. In Isabelle/HOL, definable symbols are types and constants. The latter may be ad-hoc overloaded, i.e. have different definitions for non-overlapping types. We prove that symbols that are independent of a new definition may keep their interpretation in a model extension. This work revises our earlier notion of model-theoretic conservative extension and generalises an earlier model construction. We obtain consistency of theories of definitions in higher-order logic (HOL) with ad-hoc overloading as a corollary. Our results are mechanised in the HOL4 theorem prover.

翻译：新的符号的定义只是逻辑框架中的缩略语,而且由于新的定义,任何新的事实(关于以前定义的符号)都不应存在。在伊莎贝尔/HOL中,可定义的符号是类型和常数。后者可能是临时超载的,即对非重叠类型有不同的定义。我们证明,独立于新定义的符号可以将其解释保留在模式扩展中。这项工作修改了我们早先的模型理论保守扩展概念,并概括了较早的模型构建。我们获得了更高等级逻辑定义理论的一致性,而自动超载则是一个必然结果。我们的结果在HOL4理论中被机械化。