Like HOL it is also used for verification. I believe that the Boyer-Moore prover has been more widely used than HOL in the verification of software. Thousands of programs have been proven to meet specifications using the Boyer-Moore prover. This includes compilers, assemblers and C programs compiled to 68020 machine instructions. The system either accepts or rejects each statement as it is given.
Socratic proofs are also more human readable as proof texts.
The primary inference mechanism is term rewriting together with a large collection of heuristics for performing mathematical induction. This is a mature and fairly widely used foundational system. The underlying logic is derived from Martin Lof type theory and is based on the Curry-Howard isomorphism between formulas and types. The user interface is an LCF descendent based on user defined tactics for goal reduction. It has been used to verify a variety of theorems in number theory as well as hardware and software verification.