It is common in different places to use different conventions for operator symbols, for example:
¬ - negation
∨ - disjunction
∧ - conjunction
⇒ - implication
⇔ - equivalence
It would be nice if uses could change the set of systems used to one of several possible presets.