| 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 |