isabelle: File revisions

src/Pure/type_infer_context.ML

2012-09-29	wenzelm	2012-09-29	more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;	file \| diff \| annotate
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);	file \| diff \| annotate
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;	file \| diff \| annotate
2011-11-10	wenzelm	2011-11-10	pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;	file \| diff \| annotate
2011-11-09	wenzelm	2011-11-09	tuned signature; tuned;	file \| diff \| annotate
2011-06-08	wenzelm	2011-06-08	more robust exception pattern General.Subscript;	file \| diff \| annotate
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;	file \| diff \| annotate

isabelle