  Definition packages in theorem provers provide users with means of defining
and organizing concepts of interest. This system description presents a new
definition package for the hybrid systems theorem prover KeYmaera X based on
differential dynamic logic (dL). The package adds KeYmaera X support for
user-defined smooth functions whose graphs can be implicitly characterized by
dL formulas. Notably, this makes it possible to implicitly characterize
functions, such as the exponential and trigonometric functions, as solutions of
differential equations and then prove properties of those functions using dL's
differential equation reasoning principles. Trustworthiness of the package is
achieved by minimally extending KeYmaera X's soundness-critical kernel with a
single axiom scheme that expands function occurrences with their implicit
characterization. Users are provided with a high-level interface for defining
functions and non-soundness-critical tactics that automate low-level reasoning
over implicit characterizations in hybrid system proofs.
