tidied up the tracing output

streamlined the tptp output

removed unused code

Tuned comment.

Rewrote function remove_suc, since it failed on some equations produced by recdef.

write_dimacs_sat_file now generates slightly smaller files

revised examples

code streamlining

Ressurect seq attribute accidently removed

Sort search results in order of relevance, where relevance = a) better if 0 premises for intro or 1 premise for elim/dest rules b) better if substitution size wrt to current goal is smaller Only applies to intro, dest, elim, and simp (contributed by Rafal Kolanski, NICTA)

Inttab.defined;

some structured proofs on completeness;

more contribs;

tuned;

isatool fixheaders;

with_path;

added list of theorem changes to NEWS added real_of_int_abs to RealDef.thy

added defined;

simplified union;

tuned match, unify;

tuned instantiate (avoid subst_atomic, subst_atomic_types); Logic.incr_tvar;

tuned defs interface;

moved incr_tvar to logic.ML; added eq_var, eq_tvar, instantiate, instantiateT;

tuned norm_sort, mg_domain;

tuned instantiate interface; Logic.incr_tvar;

incr_tvar (from term.ML), incr_indexes: avoid garbage;

added has_duplicates; tuned qsort;

tuned interfaces declare, define, finalize, merge: canonical argument order, produce errors; tuned checkT';

Logic.incr_tvar;

retract accidental user commit; removed obsolete XSYMBOL_HOME; tuned;