As part of my project on Boolean simplification, I propose to make the
canonical ordering of (not x) work like the canonical ordering of box, so
that the terms x and not(x) will appear in the same place when the
expression is canonicalized.
This just requires changing '(mbox mlabox) in simp.lisp/great to '(mbox
mlabox mnot) in two places.
Any objections?
Note that this is orthogonal to the question of when to treat AND/OR as
commutative and when not for cases like (x=0 or 1/x=3).
-s