needed to change the hasCode of lambda.Var and lambda.Abs to ignore the variable name. Otherwise the implication x.equals(y) implies x.hashCode()==y.hashCode() does not hold for alpha equal formulas like px = (all x P(x)) and py = (all y P(y)). This violation leads to nasty behaviour with collections (e.g. depending if you use a Map or HashMap, adding the key px after py into the map overwrites the first entry or not). Fixed a TODO in hol2fol mentioning the lack of normalization functions. With the hashCode bug fixed, it is now sufficient to systematically rename free variables (or bind them) to use the term as key in a map. LLK supports now autopropositional and non-atomic tautological axiom expansion.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@2214 85d21ef8-add0-11de-ae77-5bfb9c5a3f34