Get reductionEval to compile under mosml.

Knock-on change from 2c29276d6 (similar to e78efa92e)

ThmSetData passes thms *and* names to consumers

The names were always available, but the API now changes so that
consumers get names as well as theorem values. They can ignore the
names of course. (In this context, consumers are things like the
stateful rewriter, the monotonicity rule database, the TFL congruence
rule database etc.)

This will be helpful in allowing the stateful simpset to know what its
theorems are called, which is progress with Github issue #313 (to allow
easy removal of rewrites from a call to the simplifier).

Adjust (and reduce) interface to ThmSetData.

The change is to add an extra string parameter to the callback
function that the client provides. This is the name of the theory
which has stored the theorems. This change prompted the changes to
computeLib, IndDefLib and DefnBase.

The reduction was to remove the ThmSetData's new function, forcing
BasicProvers to use new_exporter. This was possible because of the
extra information provided to its call-back.

I also wrote some test-cases mimicking the original problem that
Magnus and Ramana had, and prettied the warning output.

This closes #73.

Preliminary thoughts on using relsimp fragments in my lambda-calculus code.

The new BETA_ss does the right thing (enables rewriting wrt beta-
equivalence), but actually adjusting the existing proofs to use this
presentation of the technology seems like undue hard work right now.

Fix another breakage caused by me changing names in chap2Theory.

Export bstore_thm from reductionEval, and use it in a few more places.

(This is the function that stores a theorem, and adds it to the stateful
lambda-calculus rewriter.)

Fix compilation error caused by change to SSFRAG's filter field.

Provide and use a new loadable-theory-data entry point.

This function, new_exporter, makes it even easier to export theorems in a
theory segment.

Slightly polish ThmSetData, and start to use it in lambda example.

Move some theorems around; mainly to put cfindleast into churchnumTheory.

Demonstrate the easy closure properties for recursive sets (empty,
UNIV, and finite sets are recursive; they are closed under union,
complement and intersection).

Make much use of the fact that it is legitimate to rewrite with
beta-reduction under the bnf_of function:

M == N ==> (bnf_of M = bnf_of N)

Adding this to my weakening congruences did break the proof of one of
my Halting Problem theorems, but a little abbreviation hackery solved
that.

Weak-head reduction (like all the others) can't create new free
variables. Also add the substitutivity result for w.h. as a
congruence rule.

More support for weak head reduction, including a simpset for
rewriting with it.

Use the new add_relsimp facilities in simpLib to implement the system
provided by reductionEval, and to simplify the proofs in chap2Script.
While I'm at it, add definitions and characterising theorems about
combinators B, C, and Y in chap2Theory.

Changes so that the weakened rewriting of lambda-terms now happens
with respect to beta-equality (==), rather than beta-reduction
(-b->*). This gives us access to more rewrites. In particular, we
get things like
church (SUC n) @@ z @@ f == f @@ (church n @@ z @@ f)
which is a nice recursive characterisation of what church numerals do,
and saves us from having to do too many ghastly things with FUNPOW.
With the above equation, neither side reduces to the other (they have
a common reduct of course), and so it wasn't a usable rewrite when
using -b->*.

In addition, to the above, I set up a natrec combinator, which would
get typed
: 'a -> (num -> 'a -> 'a) -> num -> 'a
if we were in a typed world. This combinator gets access to the value
of the recursive argument, making predecessor easier to define.

Also, give an equation like the one above for church for the cDB
function.

Many proofs are shorter. Some are slower, but the shortness of
expression won me over.

Fix for handling of conditional rewrites for beta-reduction.

Fix reductionEval so that I can have conditional rewriting wrt
beta-reduction. I.e., something along the lines of
|- P ==> M -b->* N
will successfully 'rewrite' M to N after successfully discharging P.
Proofs in the computability directory get *considerably* shorter,
particular the characterisation of the ceqnat relation.

Symbolic evaluation for beta and normal order reduction is coming
along well. The proofs in bool are much nicer. The
churchnumScript.sml is broken until I get implement conditional
rewriting in my rewriter for beta-reduction (should be easy). The
proofs there should become considerably nicer.

Fully support weaker relations than equality that aren't also
constants. Start to implement a reduction engine for beta-reduction
in the lambda-calculus. Still some wrinkles to work out.