doc-src/Tutorial/Misc/arith1.ML

Removing the datatype declaration of "order" allows the standard General.order
to be used. Thus we can use Int.compare and String.compare instead of the
slower home-grown versions.

Goal "[| ~ m < n; m < n+1 |] ==> m = n";