Tried the new addss in many proofs, and tidied others involving simplification.

Precedence of infixes is now 4 (just above that of :=)

Addition of wrappers for integration with the simplifier. New infixes setwrapper compwrapper addbefore addafter. New function getwrapper. The wrapper is a tactical that is applied to the step tactic. By default it is the identity. Using THEN one can cause other tactics to be tried before or after the step tactic. Other effects are possible using ORELSE, etc.