src/Pure/Tools/rule_insts.ML
2016-05-23 wenzelm 2016-05-23 embedded content may be delimited via cartouches;
2015-12-31 wenzelm 2015-12-31 more precise context -- potentially relevant for Eisbach dummy thm;
2015-12-16 wenzelm 2015-12-16 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-07-08 wenzelm 2015-07-08 Variable.focus etc.: optional bindings provided by user; Subgoal.focus command: more careful treatment of user-provided bindings;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-06-14 wenzelm 2015-06-14 tuned signature;
2015-06-07 wenzelm 2015-06-07 tuned signature;
2015-06-01 wenzelm 2015-06-01 discontinued legacy;
2015-03-30 wenzelm 2015-03-30 tuned;
2015-03-30 wenzelm 2015-03-30 more uniform syntax for named instantiations;
2015-03-29 wenzelm 2015-03-29 tuned signature;
2015-03-29 wenzelm 2015-03-29 more standard Sign.typ_match: sorts should be alright in result of Syntax.check_terms;
2015-03-29 wenzelm 2015-03-29 clarified context;
2015-03-29 wenzelm 2015-03-29 rule_insts_schematic is considered legacy and false by default;
2015-03-29 wenzelm 2015-03-29 tuned;
2015-03-28 wenzelm 2015-03-28 clarified goal context;
2015-03-28 wenzelm 2015-03-28 prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;
2015-03-27 wenzelm 2015-03-27 proper Rule_Insts.read_term, e.g. to enable case_tac using "_";
2015-03-27 wenzelm 2015-03-27 clarified goal context;
2015-03-25 wenzelm 2015-03-25 dummies may depend on goal params as well;
2015-03-24 wenzelm 2015-03-24 clarified name;
2015-03-24 wenzelm 2015-03-24 option to control old-style schematic mode;
2015-03-24 wenzelm 2015-03-24 admit dummy patterns in instantiations; clarified context;
2015-03-23 wenzelm 2015-03-23 implicit goal parameters are improper;
2015-03-23 wenzelm 2015-03-23 local fixes may depend on goal params;
2015-03-23 wenzelm 2015-03-23 support 'for' fixes in rule_tac etc.;
2015-03-22 wenzelm 2015-03-22 tuned;
2015-03-22 wenzelm 2015-03-22 tuned;
2015-03-20 wenzelm 2015-03-20 tuned;
2015-03-20 wenzelm 2015-03-20 read instantiations uniformly for rules and tactics; tuned;
2015-03-20 wenzelm 2015-03-20 removed presumably pointless detail;
2015-03-20 wenzelm 2015-03-20 tuned;
2015-03-20 wenzelm 2015-03-20 tuned;
2015-03-20 wenzelm 2015-03-20 make SML/NJ happy;
2015-03-20 wenzelm 2015-03-20 tuned signature;
2015-03-20 wenzelm 2015-03-20 tuned signature;
2015-03-20 wenzelm 2015-03-20 tuned -- prepare instantiation more uniformly;
2015-03-19 wenzelm 2015-03-19 more position information;
2015-03-19 wenzelm 2015-03-19 misc tuning;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-05 wenzelm 2015-03-05 tuned -- more explicit use of context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-08-21 wenzelm 2014-08-21 discontinued odd "temporary" workaround from 2006 (6ac7a4fc32a0), which has no measurable relevance;
2014-01-27 wenzelm 2014-01-27 tuned;
2014-01-26 wenzelm 2014-01-26 tuned signature;
2014-01-25 wenzelm 2014-01-25 explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
2014-01-22 wenzelm 2014-01-22 tuned signature;
2013-09-18 wenzelm 2013-09-18 more antiquotations; tuned signature;
2013-09-18 wenzelm 2013-09-18 moved module into plain Isabelle/ML user space;