Me gustaría saber acerca de los subtipos Isabelle / HOL. Explico un poco sobre por qué es importante para mí en mi respuesta parcial a mi última pregunta SO:

Intentar tratar clases y subtipos de tipos como conjuntos y subconjuntos

Básicamente, solo tengo un tipo, por lo que podría ser útil si pudiera explotar el poder de los tipos HOL a través de subtipos.

He realizado búsquedas en la documentación de Isabelle, en la Web y en las listas de correo de Isabelle. La palabra "subtipo" se usa, aunque no mucho, y parece que no es una parte muy importante del vocabulario de Isabelle.

En parte, solo me gustaría saber cómo usar la palabra "subtipo" correctamente. No quiero llamar a algo un subtipo en Isabelle que no sea un subtipo.

Según el Wiki, el subtipo es específico del idioma:

https://en.wikipedia.org/wiki/Subtyping

Importante última parte; los comandos por favor

¿Alguien me puede dar una lista de los comandos de Isar que crean los subtipos de Isar? Estoy investigandotypedef, tal como se explica en la pregunta vinculada anteriormente. Me inclino a llamar a ese subtipo, peroisar-ref.pdf no usa "subtipo" al explicar el comando.

Si hay otras formas de crear los subtipos Isabelle / HOL, me gustaría saberlo.