added sort_distinct;
removed obsolete unique_strings;

added container-lemma fresh_eqvt


(definition: container-lemma contains all instantiations
of a lemma from the general theory)

I think the earlier version was completely broken
(not sure about this one)

tuned more proofs

new lemmas

re-arranged tuples (theory * 'a) to ('a * theory) in Pure

re-arranged tuples (theory * 'a) to ('a * theory) in Pure

hashing to eliminate the output of duplicate clauses

hash tables from SML/NJ

re-arranged tuples (theory * 'a) to ('a * theory) in Pure