reserve_words : string list -> unit
- SYNOPSIS
-
Add given strings to the set of reserved words.
- DESCRIPTION
-
Certain identifiers in HOL are reserved, e.g. `if', `let' and `|',
meaning that they are special to the parser and cannot be used as ordinary
identifiers. A call reserve_words l adds all strings in l to the list of
reserved identifiers.
- FAILURE CONDITIONS
-
Never fails, regardless of whether the given strings were already reserved.
- SEE ALSO
-
is_reserved_word, reserved_words, unreserve_words.