| Fri, 24 May 2013 17:04:04 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 24 May 2013 17:00:46 +0200 | wenzelm | tuned signature; | changeset | files |
| Fri, 24 May 2013 16:42:57 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 24 May 2013 15:32:02 +0200 | wenzelm | unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!"); | changeset | files |
| Fri, 24 May 2013 15:13:25 +0200 | wenzelm | tuned signature -- slightly more general operations (cf. term.ML); | changeset | files |
| Fri, 24 May 2013 14:31:44 +0200 | wenzelm | re-use Pattern.unify_types, including its trace_unify_fail option; | changeset | files |
| Fri, 24 May 2013 14:00:10 +0200 | wenzelm | tuned signature; | changeset | files |
| Fri, 24 May 2013 16:43:37 +0200 | blanchet | improved handling of free variables' types in Isar proofs | changeset | files |