align numeric syntax: 'great' becomes 'greater' The earlier names are inconsistent with numSyntax and less descriptive.

The changes are:
intSyntax.great_tm -> intSyntax.greater_tm
intSyntax.dest_great -> intSyntax.dest_greater
intSyntax.mk_great -> intSyntax.mk_greater

int_arithTheory.add_to_great -> int_arithTheory.add_to_greater

realSyntax.great_tm -> realSyntax.greater_tm
realSyntax.dest_great -> realSyntax.dest_greater
realSyntax.mk_great -> realSyntax.mk_greater

github issue #629

More work on getting better simplification/normalisation over reals

Add fns for real$pow to realSyntax; sort listings in .sig file also

Functions for min and max added.

A couple of bug fixes for these syntax manipulation functions:
* strip_mult was utterly wrong
* list_mk_{plus,mult} were building terms in the wrong order

Provide a function for returning the integer of a real number term,
as long as that term is actually an integer (i.e., of the form &n or
~&n for some natural number numeral n).

Finished basic syntax support for the reals.

Slightly more than half an implementation of the obvious syntax functions
for the reals. Note that I have (arbitrarily) decided that 1 / 3 doesn't
qualify as a real "literal", though it has no better canonical form.
I may change my mind on this, or be open to persuasion.
Feel free to finish this off while I'm in bed :-)