extra semicolons removed from (some) .sig files

{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.

Added some test cases due originally to JRH (via Konrad) and discovered
a bug in Cooper's handling of conditional expressions. Fixed the
problem by making some code from IntDP_Munge visible.

Tests revealed that it was much better to let the Canon functions remove
implications and bi-implications themselves rather than doing this first.
Also publish the useful dealwith_nats function from IntDP_Munge.

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.