FDL
>
PVS
>
Prelude
>
naturalnumbers
> nat
: nonempty-type-eq-decl
nat : NONEMPTY_TYPE =
naturalnumber