More informative error message on weak quantifier rules.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@2249 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fixing the conditions on the substitution code. Previously, whenever it was identified that a variable v was in the domain, a new substitution was created, without the rule v -> t, and the recursive call was made. The error is that this v might also occur in the range, which meant there was a variable capture, that went unnoticed. Take for example the substitution [x -> y, y -> z], applying this to a term \y.T needs to take into account both situations (y in domain and y in range).

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@2250 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
adding unit test for bug fixed in r2250

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@2251 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
svn:ignor'ing automatically generated files and directories

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@2252 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Reworked DrawExpansionTree in prooftool so that it now uses MultiExpansionTrees. There might still be some artifacts of the old implementation in there.


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