2011-04-19 agoadded more elementary Skip_Proof.make_thm_cterm;
wenzelm [Tue, 19 Apr 2011 22:08:42 +0200] rev 42409
added more elementary Skip_Proof.make_thm_cterm;

2011-04-19 agoexplicit markup for loose bounds;
wenzelm [Tue, 19 Apr 2011 21:55:42 +0200] rev 42408
explicit markup for loose bounds;

2011-04-19 agoprefer internal types, via Simple_Syntax.read_typ;
wenzelm [Tue, 19 Apr 2011 21:33:56 +0200] rev 42407
prefer internal types, via Simple_Syntax.read_typ;

2011-04-19 agoeliminated obsolete Proof_Syntax.strip_sorts_consttypes;
wenzelm [Tue, 19 Apr 2011 21:19:14 +0200] rev 42406
eliminated obsolete Proof_Syntax.strip_sorts_consttypes;

2011-04-19 agosplit Type_Infer into early and late part, after Proof_Context;
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;

2011-04-19 agominor tuning and modernization;
wenzelm [Tue, 19 Apr 2011 16:13:04 +0200] rev 42404
minor tuning and modernization;

2011-04-19 agoslightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm [Tue, 19 Apr 2011 15:58:05 +0200] rev 42403
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;

2011-04-19 agosimplified check/uncheck interfaces: result comparison is hardwired by default;
wenzelm [Tue, 19 Apr 2011 14:57:09 +0200] rev 42402
simplified check/uncheck interfaces: result comparison is hardwired by default;
tuned;

2011-04-19 agoupdated some theory primitives, which now depend on auxiliary context;
wenzelm [Tue, 19 Apr 2011 10:50:54 +0200] rev 42401
updated some theory primitives, which now depend on auxiliary context;

2011-04-19 agomore precise treatment of existing type inference parameters;
wenzelm [Tue, 19 Apr 2011 10:37:38 +0200] rev 42400
more precise treatment of existing type inference parameters;
tuned;