The underlying type theory of HOL/Isabelle Is there a good source on the type theory of HOL/Isabelle/other HOL-based LCF-style theorem provers?
I don't think Isabelle's implementation manual is a good place to look at this. It may certainly contain links to the explanation but you can find instead a pedagogical introduction in section 2 of this thesis.