IMHO I’d expect the opposite, but I don’t actually know. Historically, Isabelle has more automation, and part of the reason is that its automation can execute faster. OTOH, Coq has a more expressive logic and type system — try writing an Isabelle type for the elements of an n-dimensional vector space.