| 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 |
| Sun, 12 Sep 2010 19:55:45 +0200 | wenzelm | common Type.appl_error, which also covers explicit constraints; | changeset | files |
| Sun, 12 Sep 2010 19:04:02 +0200 | wenzelm | eliminated aliases of Type.constraint; | changeset | files |
| Sun, 12 Sep 2010 17:39:02 +0200 | wenzelm | tuned; | changeset | files |