generalized type of inter; added substract; economize heap usage;

added previous;

added begin_theory, end_theory;

added certify_prop, cert_term, cert_prop;

datatype thmref = Name ... | NameSelection ...; added print_theorems_diff; tuned;

added member, option_ord;

OrdList.inter;

tuned;

improved treatment of intermediate checkpoints: actual copy instead of extend, purge after end; tuned;

added add_fixrec_i, add_fixpat_i; ThyParse obsolete; Sign.read_prop, Sign.cert_prop;

proper header;

get_thm(s): Name;

get_thm instead of obsolete Goals.get_thm; improved msg;

HOL-Matrix: plain session;

removed obsolete print_depth;

be less ambitious about the author's name; tuned generated root.tex;

exclude pghead.pdf from doc;

improved formatting;

use Tools/ATP/VampCommunication.ML;

Added VampCommunication.ML. Changed small set of Spass rules to Ordered version. Fixed printing out of resolution proofs if parsing/translation fails.

moved configure to lib/scripts;

./configure obsolete on virtually all systems, but apt to cause problems;

using TPTP2X_HOME; indentation, etc

fixed a faulty proof

moving some generic inequalities from integer arith to nat arith

(moved to Distribution/lib/scripts)

added fixheaders

improved comment;

some minor adaptions to make it work again;

tuned;

tuned remove;

added member;