LOCAL-VAR-AXIOMS ::= local-var-axioms VAR-DECL+ AXIOM+
A localization LOCAL-VAR-AXIOMS of variable declarations to a list of axioms is written:
vars VD1; ...; VDn · F1 ... · Fm;The sign displayed as ` · ' may be input as `·' in ISO Latin-1, or as `.' in ASCII.
It declares variables for local use in the axioms F1, ..., Fm, but it does not contribute to the declared signature. A local declaration of a variable is equivalent to adding a universal quantification on that variable to all the indicated axioms.