use Arthan's new_specification in the stateless syntax

instead of new_basic_definition.
of course, this breaks everything.
replace new_basic_definition_correct with new_specification_correct

i.e. update the stateless semantics for the new principle of constant
definition. but haven't yet updated INFINITY_AX dependencies (which
include a bunch of defined constants).
fix psholSemanticsTheory for new constant definition
update stateful hol syntax with new new_specification

translation to stateless not yet updated
fix definition of Const1, and make it an abbrev

previously wasn't distinguishing the type of the constant from the type
of its definition term
start on updating holSemantics for new new_specification

up to the main theorem, proves_IMP
tweak stateless syntax, and add new term_ok rule

change the representation of a defined constant tag to just include the
name and the definition term (rather than the whole equation term).

need to add term_ok for defined constants separately, because the new
theorem might be an implicit definition that doesn't mention the
constant (so wouldn't get picked up by the term in theorem ==> term_ok
rule).
add same new term_ok rule to stateful syntax
more work on updating holSemanticsTheory
first new_specification case of proves_IMP
finish getting holSemanticsTheory to build again

the rest of the implementation (hol_{kernel,verification} and
ml_hol_kernel) still needs updating.
update README slightly

these files will probably need just a bit more reorganisation once this
branch is merged. modelSet and sholSemantics should be deleted.
add implementation of new_specification to hol_kernel

now hol_verification needs to be updated
finish hol_verification of new_specification
failing attempt to translate new_specification

switch to pure first_dup instead of the stateful check_all_distinct, but
it still doesn't translate
move is_model_def into polySetScript.sml
use MEMBER instead of MEM, to get first_dup to translate

everything builds now.
delete the old stateless semantics
slow work towards COMPILER_RUN_INV_INR

not completely sure about the final cheat, but the others seems
plausible.
prove is_set_theory holds for a specific example

based on the universe of :'a list.

existence proved by using the natural encoding of finite sets, via the
binary numerals for the lengths of the lists (and taking all the list
elements to be equal).

but the type variable means it won't be inconsistent to assume that
there is actually an infinite set, as will be necesary to further show
that is_model holds.