The main upside Isabelle has over other proof assistants is the existence of Sledgehammer: invoke it, and your current proof state gets handed off to a SMT solver like cvc4, veriT, z3, vampire, etc. If the SMT solver finds a solution, Isabelle then reconstructs the proof.
It's essentially a brute-force button that no other proof assistant (aside from Coq) has.
It's essentially a brute-force button that no other proof assistant (aside from Coq) has.