The HOL-4 Trust Story. The LCF style of theorem prover implementation is embodied in HOL-4 by its abstract datatype of theorems. We first review this approach before going on to discuss several modifications and extensions of it: (1) The `lazy' theorems of Boulton were aimed at speeding up proof-producing decision procedures. (2) The challenge of integrating a BDD package into HOL-4 prompted Gordon and Amjad to recapitulate an LCF-style BDD kernel upon which to construct model-checkers. (3) Tagged theorems may be implemented in the meta-language (Kalvala) or in the object language (Norrish, Slind). (4) Gordon, Hunt, Kaufmann, and Reynolds have created a link between HOL-4 and ACL2. We will examine the trust story that emerges and discuss future opportunities.