Fix idvalue output and PGML print mode raw encode/decode.

permitting empty datatypes

improved handling of nat numerals

tuned code theorems for ord on integers

simplified code generator setup

tuned code theorems

added add_numerals_of

now using "class"

using "fst" "snd" for Haskell code

added code theorems for UNIV

adjusted to latest changes

new code theorems

syntax for "class attach const"

prefix of class interpretation not mandatory any longer

Meson.is_fol_term now takes a theory as argument. Minor tidying.

New code to store theorem names in a concise form rather than as fully-qualified. Meson.is_fol_term now takes a theory as argument.

The first-order test now tests for the obscure case of a polymorphic constant like 1 being used with a function type.

abbrev: be permissive after transformation;

exported get_ss, map_ss;

tuned;

tuned ML setup;

added @{const_name}, @{const_syntax};

more cleanup

Add closeblock/openblock structure to proof-block commands

Updated success string for Vampire. eprover no longer sought in the PROVER directory. eprover now gets tstp input. Streamlined the code a bit.

Now outputs metis calls

added headers

cleanup, fixing sml/nj related problems

gensym: removed bits of dead code;

gensym no longer includes ' or _ in names (trailing _ is bad)