- SYNOPSIS
-
The type variable `:B`.
- DESCRIPTION
-
This name is bound to the HOL type :B.
- FAILURE CONDITIONS
-
Not applicable.
- USES
-
Exploiting the very common type variable :B inside derived rules (e.g. an
instantiation list for inst or type_subst) without the inefficiency or
inconvenience of calling a quotation parser or explicit constructor.
- SEE ALSO
-
aty, bool_ty.