Moved hol-light's wellorder theorems into HOL4's wellorderTheory

Remove TABs from src

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

Remove -- as an alias for Term parser.

As per comment in release notes this has long been replaced as
appropriate style.

Remove unnecessary structure bracketting

As per 89fc99bc3, but on as many examples as a grep -R can find.

Delete trailing whitespace

using new lemmas to prove existing theorems easier

using LESS_ALT to prove WF_LESS more easily

use of LESS_ALT to give shorter proofs

LESS_ALT, alternative definition of <

inverse of LESS_MONO

shorter proof of LESS_MONO

requires moving definition of PRE forward

new proof of LESS_0

uses existing proof of LESS_0_0, doesn't require LESS_THM

Make a couple of important termination theorems automatic rewrites.

In particular:

|- WF $<
|- inv_image R f x y <=> R (f x) (f y)

add some more OpenTheory names to the map

add various names to the OpenTheory map

This is in preparation for logging llistTheory.

Notes:
- Sent combin$C to Function.Combinator.c (same for combin$S).
Another name might be preferred on the OpenTheory side.
- Not sure what bool$BOUNDED is about; dumped it in the HOL4 namespace.
- Put lots of pred_set constants in the Set namespace, but in the
standard (OpenTheory) library it seems like Set is for constants
operating on an abstract type of sets (rather than predicates). I'm
not sure whether we should use a different namespace when working with
sets-as-predicates or just pretend predicates are the abstract type
and do a bit of magic on article reading/writing as necessary (don't
know what that would be exactly yet).
- Similar for constants in set_relation, which I'm currently putting in
the Relation namespace. Although it looks like currently OpenTheory
doesn't use an abstract type of relations (but probably it will
later).
- Sent marker$Cong and marker$Abbrev to Unwanted.id, but not sure if
Unwanted.id is supposed to be polymorphic (whereas those are identity
functions restricted to bool). Similar for numeral$iZ
- sent GSPEC to Set.specification; maybe not an obvious name...
- Using top-level "While" namespace for whileTheory
- dumped numeral$iiSUC in HOL4 namespace; not sure what to do with it
- BIT2 is going to Number.Numeral.bit2; this is in line with wanting the
base library to be liberal, i.e. a union of all useful basic constants
and theorems (so has bit0, bit1 and bit2)... but I think there may be
competing goals for base

Make a couple of theorems about prim_rec$measure automatic rewrites.

Delete unnecessary infix declarations in prim_recScript.sml.

Attempt to tidy-up HOL's output in non-interactive mode - mostly through lining
up definition and theorem names.

TeX macros in TeX_notation calls need to be terminated with {}.

Move more TeX notations into appropriate theory files.

Word-related notation still to do.

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

Did some community service expunging all occurrences of the old syntax for
if-then-else from the HOL distribution.

Apologies if I've broken your example or development: you can either upgrade
it to use the new syntax or else issue the magic parser incantation that
I chopped out of boolScript.sml on this check in.

Change to type of new_specification, and made it tell that parser about
the introduced constants. Lots of knock-on (trivial) mods.

Various bits of messing about.

paired syntax.

Changes making directory Kananaskis compatible.

Further simplifications of number theory to remove dependence on
axiom of choice.

Changes due to the incorporation of John Harrison's datatype definition
package.

Change to structure of numLib so that reduce and arith are incorporated.