| Sat, 08 Nov 2014 22:10:16 +0100 | wenzelm | removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich); | changeset | files |
| 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 |