The underlying type theory of HOL/Isabelle
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.