Allow Unicode lambda (λ, U+03BB) in src/

This is because writing things like (\(x,y). x + y) puts editor modes
into strange states when they think the second left-parenthesis has
been "escaped". Allowing a lambda to be used here gives us a chance to
avoid confusing editors, and who wouldn't want that?

Cleanup of append thms for SORTED

Implement new Definition syntax; use it in src/sort and Tutorial

Reconcile store_thms with diverging names in db and val binding

Opening lcsymtacs is no longer necessary.

All l/case short simp tacs use LET_ss + ARITH_ss

This means that fs and rfs pick up LET_ss and ARITH_ss, making them
indistinguishable from the 'l' versions.

update mergesortTheory after redundant theorem removed

Remove some Unicode in src/

Remove some trailing whitespace.

A theory of mergesort

Mergesort based on the algorithm used in OCaml. There are two versions.
mergesort_tail uses a tail recursive merge (following OCaml) whereas
mergesort uses a normal merge. Both are stable.

Initial experiments show that mergesort outperforms QSORT and QSORT3
executing with EVAL.

I ran each of the 4 sorts on 3 different lists of 10000 numbers. Call
them SORTED (COUNT_LIST 10000), RAND32 (10000 random 32bit numbers), and
RAND16 (10000 random 16bit numbers). NB, QSORT is not stable whereas
QSORT3 is.

mergesort mergesort_tail QSORT QSORT3
SORTED 10.9s 13.4s * *
RAND32 27.6s 30.7s 33.8s 1m23s
RAND16 18.2s 20.5s 21.4s 55.4s

* QSORT and QSORT3 do not finish on the sorted input for (COUNT_LIST
500) they take 10.8s and 31.4s respectively. This is because quicksort
exhibits its quadratic worst-case behaviour on already sorted inputs.