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

add_path for naming in proof contexts

locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes

slightly tuned

slight cleanup

adjusted code lemmas

continued

dropped diagnostic switch

Improved handling of situation when theorem in cache disagrees with theorem supplied: new clauses are now returned, fixing a bug in the metis method.

Fixed print translations for quantifiers a la "ALL x>=t. P x". These used to fail when the other term in the comparison was itself a bound variable, as in "EX y. ALL x>=y. P x".