tuned

no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property

generate nicer 'set' theorems for (co)datatypes

compile

took out test driver

make TPTP tools work on polymorphic (TFF1) problems as well

put comments between TPTP lines to comply with TPTP BNF

test driver

treat variables as frees in 'conjecture's

support TFF1 in TPTP parser/interpreter

tuning

tuned

tuned

tuned

merged

handle deep nesting in N2M

made tactic more robust

added lemma

replaced misleading - by _

more correct clique computation for N2M

regenerated ML-Lex/Yacc files

correctly interpret arithmetic types

added 'datatype_compat' tests

tuning whitespace

tuned skolemization

rationalize Skolem names

tuning

tuned code

don't rename variables which will be renamed later anyway

normalize skolem argument variable names so that they coincide when taking the conjunction

tuning

tuned comments

deal with E definitions

updated 'compress' docs

cleaner 'compress' option

renamed 'sh_minimize' to 'minimize'; compile;

restored more sorting

tuned terminology (cf. 'isar_proofs' option)

sort facts in minimizer as well

default on 'metis' for ATPs if preplaying is disabled

more informative preplay failures

rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures

slightly earlier exit from preplaying

honor 'dont_minimize' option when preplaying one-liner proof

Metis is being used to emulate E steps;

updated application of print_tac to take context parameter;

better duplicate detection

normalize conjectures vs. negated conjectures when comparing terms