HOL uses two global grammars to control the parsing and printing of
term and type values. These can be adjusted in a controlled way with
functions such as add_rule and overload_on. By using just these
standard functions, the system is able to export theories in such a
way that changes to grammars persist from session to session.
Nonetheless it is occasionally useful to set grammar values directly.
This change can’t be made to persist, but will affect the current
session.