wenzelm [Tue, 19 Apr 2011 21:55:42 +0200] rev 42408
explicit markup for loose bounds;
wenzelm [Tue, 19 Apr 2011 21:33:56 +0200] rev 42407
prefer internal types, via Simple_Syntax.read_typ;
wenzelm [Tue, 19 Apr 2011 21:19:14 +0200] rev 42406
eliminated obsolete Proof_Syntax.strip_sorts_consttypes;
wenzelm [Tue, 19 Apr 2011 20:47:02 +0200] rev 42405
split Type_Infer into early and late part, after Proof_Context;
added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;
wenzelm [Tue, 19 Apr 2011 16:13:04 +0200] rev 42404
minor tuning and modernization;
wenzelm [Tue, 19 Apr 2011 15:58:05 +0200] rev 42403
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm [Tue, 19 Apr 2011 14:57:09 +0200] rev 42402
simplified check/uncheck interfaces: result comparison is hardwired by default;
tuned;
wenzelm [Tue, 19 Apr 2011 10:50:54 +0200] rev 42401
updated some theory primitives, which now depend on auxiliary context;
wenzelm [Tue, 19 Apr 2011 10:37:38 +0200] rev 42400
more precise treatment of existing type inference parameters;
tuned;
wenzelm [Mon, 18 Apr 2011 23:41:15 +0200] rev 42399
pretty_abbrev: read abbreviation more directly;