There are three other systems implementing the same logic as HOL4: HOL Light, by John Harrison and written in OCaml; ProofPower, by Rob Arthan and written in SML; and HOL Zero, by Mark Adams and written in OCaml.
The HOL provided by the Isabelle system (often written “Isabelle/HOL”) is very similar to the higher order logic of HOL4, HOL Light and ProofPower, but has a type system with Haskell-like type-classes.
The PVS system has a type system with predicate sub-typing. Getting a term (formula, definition) to typecheck can require arbitrary amounts of work, but definitions are a deal more expressive.
The HOL-ω system implements a sophisticated type system (like that of System Fω) that also remains a superset of HOL4’s. In terms of implementation, the system is also a drop-in replacement for HOL4: all existing HOL4 scripts should continue to work as before in HOL-ω.