Fix src/rational for tight equality

Remove some code from schneiderUtils along the way that can't have
ever worked (and wasn't being called). Some of it included parsing
calls to ancient if-then-else syntax (gd => t | e).

Don't export ERR from HolKernel

Change irule to not include a rpt conj_tac effect

Closes #465

Fix RAT_SGN to be the same as the rat_sgn; deleting extra constant

Jeremy Dawson pointed out the overlap: RAT_SGN r was the same as
rat_of_int (rat_sgn r), and had stolen some theorem names to boot.

For the sake of backwards compatibility, I've dropped RAT_SGN
entirely, and proved the few extra theorems that I'd proved about
RAT_SGN about rat_sgn.

Reformat a bunch of proofs in rational/ratScript.sml

Pulling things back under 80 columns, making proofs less indented and
pulling them up to take up less vertical space too.

Prove more about RATN & RATD; define RAT_SGN; prove results about it

Fix Unicode in previous commit; add RATN & RATD constants to rat thy

RATN and RATD return the numerator and denominator of a rational
number, picking the numerator with the least absolute value, and
choosing 1 for the denominator if the numerator is zero. RATD returns
a natural number, and the numerator is an integer.

Fix a rational proof broken by 85a2185164

Tidy up some ratScript proofs for style (e.g., <= 80 columns)

More useful theorems about the rationals

Also make x * y = 0q the LHS of an automatic rewrite

More theorems about rational arithmetic when expressed as fractions

Untabify rationalScript.sml

Make more rational theorems automatic; define rat min and max

Make more rat theorems automatic rewrites

Make a bunch of rat theory rewrites automatic; define rat_of_int

Remove eqtype declaration for term type

Preserve add_user_printer properly in grammar data

This requires a slightly involved process for storing references to
code in theory files.

Update the .doc file on add_user_printer (which was already incredibly
long), and add a test.

Closes #367

RAT_AINV_ONE_ONE in effect already proved

shorter proof of RAT_DIV_CONG2

shorter proofs of RAT_AINV_EQ, RAT_EQ_AINV

theorems FRAC_MINV_1 and RAT_MINV_1

removed repeated proofs of RAT_AINV_EQ, RAT_EQ_AINV

Delete trailing whitespace in src/

shorter proof of RAT_MUL_RINV

miscellaneous minor speed-ups of proofs

much shorter proof of RAT_MUL_ONE_ONE

much shorter proof of RAT_ADD_ONE_ONE

theorems for <= for rationals

Stop EVAL making a mess of rational arithmetic

Use zDefine to avoid having definitions of fundamental arithmetic
operations expanded.

Remove trailing w/space in rational/ratScript.sml

shorter proof of ratTheory.RAT_MUL_CONG1

also useful lemma FRAC_MUL_EQUIV1

shorter proof of ratTheory.RAT_ADD_CONG1

also useful lemma FRAC_ADD_EQUIV1

shorter proof of ratTheory.RAT_MINV_CONG

uses new theorem ratTheory.FRAC_MINV_EQUIV

also name clash in ratScript.sml between theorem stored as rat_def and
ML identifier rat_def, changed latter to rat_thm

shorter proofs of RAT_NMRxx0_CONG in ratTheory

also useful lemmas RAT_EQUIV_NMR_xxZ_IFF

some shorter proofs for ratTheory

Give the rationals decimal fractions too.

Change & (the overloaded injection function from natural numbers into
other numeric types), to be a prefix symbol in the grammar. This
allows things like -&n to pretty-print better. There are a few
breakages here and there. I realise that the type-annotation suffix
should be looser than &'s precedence level so that &n:int parses as
(&n):int rather than &(n:int). Changing this revealed some faults in
the handling of operators like unary minus, so the construction of the
precedence matrix in term_parse needed to change a little. Changes to
later files and theories were mainly caused by people writing ``&``;
you now need to write ``$&``, or ``(&)``.

Implement unary minus (the old ~ still also works). Selftest level 2
passes. Changes in the "words world" were replacing $- with -. In
the two quotient changes, I made sure that the infix operator
that used the - character was part of the grammar before it was
parsed. This is necessary because - is now a non-aggregating
character, mainly so that ``--p`` parses as three tokens, not two. Of
course, if you added -- to your grammar, then it would go back to
parsing as two.

Fairly dramatic change, supporting the use of "syntactic patterns".
It is now possible to overload a name to term (typically a
lambda-abstraction) in order to create syntax-only definitions. For
example, there is a definition of not-equals now in the system:
val _ = overload_on ("<>", ``\x y. ~(x = y)``)
val _ = set_fixity "<>" (Infix(NONASSOC, 450))
This definition is parsed and pretty-printed.

Two other annoying changes. The interface for adding unicode variants
has changed, and I have made precedence level 450 of the parser
non-associative. This latter change has caused most of the (minor)
adjustments to the files below. The regression test doesn't go
through yet. (Currently there is a failure in
quotient/examples/sigma that I don't understand.)

Random typo.

Random other bits deemed useful.

Remove a redundant theorem - spotted by Mike.

Add more aggressive normalisation of multiplicative expressions to ARITH_ss.
Also provide old_arith_ss values for scripts that don't want this new
behaviour. Update proofs to go through again. Some should be a bit more
robust in the face of future changes to arith_ss. Others just punt and refer
to old_arith_ss.

support for numeral forms added

Initial version of theory and libraries of rational numbers added.