First, just to clarify, I wrote "Isabelle/HOL", and I'm not claiming anything about any of the many many other systems that have "HOL" in their name. I don't know those.
That said, I think the thing that annoyed me most were the different language levels: "assume P show Q" and "P ==> Q" are both implications, but somehow different. I never quite understood why and how, but there seem to be cases where only one can be proved but not the other. Similarly for different kinds of universal quantification. Your interpretation of "bizarre" may very well vary, but I found these unintuitive and not explained well in the documentation that I found.
(Don't ask for anything much more concrete than this. It's been a while, and I've forgotten the details.)
FWIW the differences are largely syntactic. Some of them are due to implication or quantification being in the meta-level (Pure, Λ/long ⇒) vs object-level (HOL, ∀/⟶). Transporting between them (for HOL) is easy and the automation tends to normalize object-level quantification and implication into meta-level.
"assume P show Q" is just Isar-syntax for a structured proof of "P ==> Q" (which is a term).
That said, I think the thing that annoyed me most were the different language levels: "assume P show Q" and "P ==> Q" are both implications, but somehow different. I never quite understood why and how, but there seem to be cases where only one can be proved but not the other. Similarly for different kinds of universal quantification. Your interpretation of "bizarre" may very well vary, but I found these unintuitive and not explained well in the documentation that I found.
(Don't ask for anything much more concrete than this. It's been a while, and I've forgotten the details.)