Mon, 13 Sep 2010 12:42:08 +0200 Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
wenzelm [Mon, 13 Sep 2010 12:42:08 +0200] rev 39295
Type_Infer.finish: index 0 -- freshness supposedly via Name.invents; Type_Infer.fixate_params: full Proof.context;
Mon, 13 Sep 2010 11:35:55 +0200 simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm [Mon, 13 Sep 2010 11:35:55 +0200] rev 39294
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip