O que é um subtipo Isabelle / HOL? Quais comandos do Isar produzem subtipos?

Eu gostaria de saber sobre os subtipos de Isabelle / HOL. Eu explico um pouco sobre por que é importante para mim na minha resposta parcial à minha última pe...