| Thu, 16 May 2013 14:58:30 +0200 | blanchet | correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer | file | diff | annotate |
| Thu, 16 May 2013 13:34:13 +0200 | blanchet | tuning -- renamed '_from_' to '_of_' in Sledgehammer | file | diff | annotate |
| Mon, 06 May 2013 11:03:08 +0200 | smolkas | handle dummy atp terms | file | diff | annotate |
| Wed, 20 Feb 2013 08:44:24 +0100 | blanchet | slacker comparison for Skolems, to avoid trivial equations | file | diff | annotate |
| Thu, 03 Jan 2013 17:10:12 +0100 | blanchet | rename variable in binder, not just in body | file | diff | annotate |
| Thu, 03 Jan 2013 15:13:11 +0100 | blanchet | swap Vampire's Skolem arguments to bring them in line with what E and metis's new skolemizer do (helps Isar proof reconstruction in some cases) | file | diff | annotate |
| Thu, 03 Jan 2013 00:02:15 +0100 | blanchet | tuned comment | file | diff | annotate |