Sets the name given to the formal model HolCheck constructs internally.
FAILURE
Fails if the first argument does not follow the naming rules for constants.
COMMENTS
This information is optional when constructing HolCheck models. It should be set if more than one model is being used in the same session, to avoid name clashes.