2008-03-19 ago avoid Auto_tac;
2007-10-11 ago rationalized redundant code
2006-11-29 ago simplified Logic.count_prems;
2006-09-15 ago tuned;
2006-08-30 ago faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
2006-03-10 ago clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
2005-10-09 ago Tactics sat and satx reimplemented, several improvements
2005-09-23 ago new sat tactic imports resolution proofs from zChaff