src/Pure/Isar/rule_insts.ML
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-16 wenzelm 2009-03-16 method parser: pass proper context;
2009-03-16 wenzelm 2009-03-16 export method parser;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-15 wenzelm 2008-08-15 Args.name_source(_position) for proper position information;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-06-28 wenzelm 2008-06-28 tuned;
2008-06-19 wenzelm 2008-06-19 private add_used (from drule.ML); Variable.declare_names;
2008-06-16 wenzelm 2008-06-16 added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML); pervasive operations; tuned;
2008-06-16 wenzelm 2008-06-16 added read_instantiate;
2008-06-14 wenzelm 2008-06-14 export subgoal_tac, subgoals_tac, thin_tac;
2008-06-10 wenzelm 2008-06-10 added (e)res_inst_tac; tuned comments;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2007-11-08 wenzelm 2007-11-08 where/of: do not allow schematic variables here!
2007-11-07 wenzelm 2007-11-07 Syntax.read_typ; rule_tac etc.: proper read_termTs (discontinued rogue type-inference);
2007-11-07 wenzelm 2007-11-07 attribute where/of: proper Syntax.parse/check;
2007-04-15 wenzelm 2007-04-15 proper ProofContext.infer_types;
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.; Term.string_of_vname;
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-11-23 wenzelm 2006-11-23 renamed Args.Name to Args.Text;
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-12 wenzelm 2006-09-12 moved term subst functions to TermSubst;
2006-09-06 wenzelm 2006-09-06 read_instantiate: declare names of TVars as well (temporary workaround for no-freeze feature of type inference);
2006-08-05 wenzelm 2006-08-05 reworked read_instantiate -- separate read_insts;
2006-08-03 wenzelm 2006-08-03 Rule instantiations -- operations within a rule/subgoal context.