This paper reports on a simpler and more powerful replacement for the principles for defining new constants that were previously provided in the various HOL implementations. We discuss the problems that the new principle is intended to solve and sketch the pro... ...
