| Sat, 08 Nov 2014 21:31:51 +0100 | wenzelm | optional proof context for unify operations, for the sake of proper local options; | changeset | files |
| Sat, 08 Nov 2014 17:39:01 +0100 | wenzelm | clarified name of Type.unified, to emphasize its connection to the "unify" family; | changeset | files |
| Sat, 08 Nov 2014 16:55:41 +0100 | wenzelm | proper Envir.norm_type for result of Type.raw_unifys; | changeset | files |
| Sat, 08 Nov 2014 16:42:04 +0100 | wenzelm | avoid slow metis proof; | changeset | files |
| Sat, 08 Nov 2014 16:35:24 +0100 | wenzelm | proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago); | changeset | files |
| Sat, 08 Nov 2014 15:45:00 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 08 Nov 2014 15:44:41 +0100 | wenzelm | updated some sledgehammer proofs -- much faster; | changeset | files |
| Sat, 08 Nov 2014 15:40:29 +0100 | wenzelm | updated sledgehammer proof after breakdown of metis (exception Type.TUNIFY); | changeset | files |