src/Pure/Isar/rule_insts.ML
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.