FDL > PVS > Prelude > finite sets def > finite_set : type-eq-decl

finite_set : TYPE = (is finite)