| Mon, 30 May 2011 15:30:05 +0100 | paulson | Workaround for hyperref bug affecting index entries involving the | symbol | changeset | files |
| Mon, 30 May 2011 13:58:00 +0200 | bulwahn | improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of | changeset | files |
| Mon, 30 May 2011 13:57:59 +0200 | bulwahn | automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option | changeset | files |
| Mon, 30 May 2011 12:20:04 +0100 | paulson | merged multiple heads | changeset | files |
| Mon, 30 May 2011 12:15:17 +0100 | paulson | Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler | changeset | files |
| Sun, 29 May 2011 19:40:56 +0200 | blanchet | always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated | changeset | files |