Checking Conservativity of Overloaded Definitions in Higher-Order Logic

摘要

Overloading in the context of higher-order logic has been used for some time now. We define what we mean by Higher-Order Logic with Conservative Overloading (HOLCO). HOLCO captures how overloading is actually applied by the users of Isabelle.