2006-01-20 mengj 2006-01-20 added some debugging code.
2005-11-28 mengj 2005-11-28 Slight modification to trace information.
2005-11-18 mengj 2005-11-18 -- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
2005-10-19 mengj 2005-10-19 *** empty log message ***
2005-10-19 mengj 2005-10-19 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").