| Mon, 29 Jul 2013 18:06:39 +0200 | blanchet | avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference | file | diff | annotate |
| Fri, 24 May 2013 16:43:37 +0200 | blanchet | improved handling of free variables' types in Isar proofs | file | diff | annotate |
| 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 |