node_trans: revert to original transaction code (pre 1.54);

use: not a theory command!

converted back from 0..< to <.

added email

tuned trace info (depth)

simplifier trace info; Suc-intervals

some adaptions

Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML. Changed watcher.ML so that the Unix.execute and Unix.reap functions are used instead of those in modUnix.ML, and consequently removed modUnix.ML from Reconstruction.thy

tuned;

string FindTheorems.criterion;