If you are already familiar with Coq or even Ocaml/Haskell style programming.

I really believe, the volume 3 of SF series is a more polished and more approachable book.

https://softwarefoundations.cis.upenn.edu/vfa-current/index....

I am halfway through the first book (doing ALL exercises), I hope by next year end I would really like to finish vol 3.

This Isabelle books seems to cover more ground though.