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

Merged hol-light's cardTheory (rich_cardinalTheory) with HOL4's cardinalTheory

Remove TABs from src

Will also make selftest to check that they aren't introduced

Delete trailing whitespace in src/

shorter proof of RAT_MUL_RINV

trailing newlines in *.{sml,sig} files from src/ removed

Trailing newlines from SML files in src/ were rendered in HTML documentation.

Remove a redundant theorem - spotted by Mike.

Initial version of theory and libraries of rational numbers added.