Added a few newlines at end of files to suppress warnings from my
Mosml -> MLton preprocessor.

{COOPER,OMEGA}_TAC now both try to use the assumptions when they run.
They're no longer just CONV_TAC {COOPER,OMEGA}_CONV. The new implementation
moves all assumptions whose non-Presburger sub-terms have type :int or :num
onto the goal, and then calls CONV_TAC.

Progress with Omega. Also refactored code for handling natural numbers
and generalising over non-presburger sub-terms so that both Omega and
Cooper can use it.