2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-15 ago Args.name_source(_position) for proper position information;
2008-08-09 ago unified Args.T with OuterLex.token, renamed some operations;
2008-06-28 ago tuned;
2008-06-19 ago private add_used (from drule.ML);
2008-06-16 ago added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
2008-06-16 ago added read_instantiate;
2008-06-14 ago export subgoal_tac, subgoals_tac, thin_tac;
2008-06-10 ago added (e)res_inst_tac;
2008-03-28 ago Context.>> : operate on Context.generic;
2008-03-27 ago eliminated delayed theory setup
2007-11-08 ago where/of: do not allow schematic variables here!
2007-11-07 ago Syntax.read_typ;
2007-11-07 ago attribute where/of: proper Syntax.parse/check;
2007-04-15 ago proper ProofContext.infer_types;
2007-04-14 ago cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2006-12-18 ago switched argument order in *.syntax lifters
2006-11-23 ago renamed Args.Name to Args.Text;
2006-09-15 ago renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-12 ago moved term subst functions to TermSubst;
2006-09-06 ago read_instantiate: declare names of TVars as well (temporary workaround for no-freeze feature of type inference);
2006-08-05 ago reworked read_instantiate -- separate read_insts;
2006-08-03 ago Rule instantiations -- operations within a rule/subgoal context.