Tidying, and getting rid of SELECT_GOAL (as it does something different now)

Added HOL-ZF to Isabelle.

substantial improvement in codegen iml

Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset. The hash table (for removing duplicate) now stores clauses as Term.term with names.

relevance_filter takes input axioms as Term.term.

Proof reconstruction now only takes names of theorems as input.

Added tptp_write_file to write all necessary ATP input clauses to one file.

tptp_write_file now takes goals and axioms as Term.term and writes them to a file.

Added functions to retrieve local and global atpset rules. cnf thms to Term.term format.

Moved the settings for ATP time limit to res_atp.ML

Merged res_atp_setup.ML into res_atp.ML. HOL translation is integrated with background Isabelle-ATP linkup. Both ATP methods and background linkup retrieve lemmas stored in claset, simpset and atpset.

When ATP methods call ATPs, all input clauses from one subgoal are written to one file.

Merged res_atp_setup.ML into res_atp.ML.

SELECT_GOAL: fixed trivial case;

fixed a typo in a comment

tuned;

method: SelectGoals;

method: syntax for SelectGoals;

text: added SelectGoals;

tuned conj_curry;

added extract, retrofit;

added mk_conjunction; tuned conj_curry;

method: restriction to first n sub-goals;

minor changes

more examples

changed and retracted change of location of code lemmas.

ignore repeated vars on lhs, cleanup

improvements for nbe