17 months ago wenzelm 2019-01-03 clarified signature: more types;
2016-12-13 wenzelm 2016-12-13 more symbols;
2015-03-29 wenzelm 2015-03-29 proper local Proof_Context.arity_sorts;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-04-06 wenzelm 2014-04-06 more source positions;
2012-09-29 wenzelm 2012-09-29 more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-04-03 wenzelm 2012-04-03 better drop background syntax if entity depends on parameters; more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);
2012-03-12 wenzelm 2012-03-12 clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
2011-11-10 wenzelm 2011-11-10 pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
2011-11-09 wenzelm 2011-11-09 tuned signature; tuned;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-04-19 wenzelm 2011-04-19 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;