| Fri, 10 Sep 2010 23:56:35 +0200 | krauss | use eta-contracted version for occurrence check (avoids possible non-termination) | changeset | files |
| Mon, 13 Sep 2010 13:20:18 +0200 | wenzelm | tuned signature; | changeset | files |
| Mon, 13 Sep 2010 12:42:08 +0200 | wenzelm | Type_Infer.finish: index 0 -- freshness supposedly via Name.invents; | changeset | files |
| Mon, 13 Sep 2010 11:35:55 +0200 | wenzelm | simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars; | changeset | files |
| Mon, 13 Sep 2010 00:10:29 +0200 | wenzelm | tuned; | changeset | files |
| Sun, 12 Sep 2010 22:28:59 +0200 | wenzelm | Type_Infer.preterm: eliminated separate Constraint; | changeset | files |
| Sun, 12 Sep 2010 21:24:23 +0200 | wenzelm | Type_Infer.infer_types: plain error instead of kernel exception TYPE; | changeset | files |
| Sun, 12 Sep 2010 20:47:47 +0200 | wenzelm | load type_infer.ML later -- proper context for Type_Infer.infer_types; | changeset | files |