wenzelm [Tue, 19 Apr 2011 22:32:49 +0200] rev 42410
less bulky "_position", for improved readability of parse trees;
wenzelm [Tue, 19 Apr 2011 22:08:42 +0200] rev 42409
added more elementary Skip_Proof.make_thm_cterm;
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;