[robinzfc]

It was a similar experience for me when I tried to learn proving with Isabelle/HOL without an expert help. I gave up and switched to Isabelle/ZF and that was easy, my standard mathematics background was sufficient. I use a subset of the Isar language that is needed for my formalized mathematics hobby (shameless plug: isarmathlib.org). Of course if your goal is software verification, then Isabelle/HOL is the way to go. Btw, Isabelle is not "the HOL based theorem prover", Isabelle/HOL is just its most popular logic.