A smaller less featured one, but very useful nonetheless. (Specifically, sledgehammer is superior as a checker and automated proof library check is also invaluable in simplification.)

Technically, Why3 (intermediate language and prover manager used in SPARK for verification) can interface with Isabelle too. I should try it out.

More edit: someone has done it, called HOL-SPARK. Excellent.