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)

tuned document;

\usepackage{amssymb};

moved some non-kernel material to more_thm.ML;

removed obsolete eq_set;

Thm.internalK;

Further operations on type thm, outside the inference kernel.

added more_thm.ML;

moved eq_thm etc. to structure Thm in Pure/more_thm.ML;

Added formalization of size-change principle (experimental).

added theorems_of;

removed obsolete theorem_space;

Added lemma lfp_const: "lfp (%x. t) = t

exported serializer parsers

proper treatment of -> as type constructor

tuned