tweak a proof slightly

for some reason it failed when I tried it on another machine.
add a couple defs to bytecode_emitScript.sml

this should have been done in 872ca68a
delete some unused stuff
prove bool theory extends init (and hence is ok)
prove extensions of bool are consistent, cheating existence of model
split bool_ctxt up and move it out into separate theories

also, make it generic, i.e. mk_bool_ctxt ctxt adds the boolean
definitions to an arbitrary initial ctxt. more general for proving
theorems about. similarly mk_eta_ctxt, mk_select_ctxt, ...
relax the constraint on standard interpretations slightly

only require the interpretation to do the right thing when given an
appropriate type valuation (i.e. one that is ARB on irrelevant tyvars)
prove one can always find a valuation
semantic characterisation of interpretations of Booleans

and thoughts on proving that any interpretation of bool_ctxt must be
correct in this sense
add selftests to the regression test script
poor attempt to speed up proof of bool_extends
work towards bool_has_bool_interpretation

probably want to change the treatment of term valuations and
inteprets_on_as so as to only ever deal with proper type valuations (and
stop fussing about with ARB).

also proved a few lemmas about the boolean signature and ok terms in it.
some more properties about STRING_SORT
WIP: more reworking of treatment of term valuations

make them apply to a list of the values of the (sorted) type variables,
to make the dependence completely explicit...
fix holConsistencyTheory for recent changes to is_term_valuation
finish proof of bool_has_bool_interpretation

this means the definitions of the boolean operations are correct (they
constrain interpretations to interpret them with the desired semantics).
this will be important when showing the axiom of infinity (which depends
on many of these constants) is consistent.
update README
prove ETA_AX consistent
fix error in SELECT_AX and then prove it consistent

this doesn't actually require is_choice, i.e. we don't have to
explicitly designate the choice function in the set theory, because we
specify the semantics of select indirectly via its axiom.
move HOL semantics and metatheory into separate directory

to make room for the implementations