src/Pure/drule.ML
2016-12-13 wenzelm 2016-12-13 more symbols;
2016-04-28 wenzelm 2016-04-28 unfold is subject to unfold_abs_def (still inactive); tuned signature;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2015-12-15 wenzelm 2015-12-15 tuned signature -- clarified modules;
2015-08-16 wenzelm 2015-08-16 produce certified vars without access to theory_of_thm, and without context;
2015-08-16 wenzelm 2015-08-16 added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);
2015-07-28 wenzelm 2015-07-28 more explicit context; tuned signature;
2015-07-28 wenzelm 2015-07-28 clarified Variable.gen_all; simplified Local_Defs.export: pointless partial application;
2015-07-28 wenzelm 2015-07-28 more explicit context;
2015-07-28 wenzelm 2015-07-28 more direct access to atomic cterms;
2015-07-27 wenzelm 2015-07-27 tuned signature; clarified context;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-27 wenzelm 2015-07-27 more explicit checks -- improved errors;
2015-07-27 wenzelm 2015-07-27 eliminated cterm_instantiate;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-27 wenzelm 2015-07-27 added infer_instantiate_vars, which allows inconsistent types for variables, as required for Metis proof reconstruction;
2015-07-26 wenzelm 2015-07-26 ignore non-existant variables, like other instantiate rules;
2015-07-26 wenzelm 2015-07-26 added infer_instantiate'; clarified boundary cases of instantiate';
2015-07-26 wenzelm 2015-07-26 more uniform exceptions, like cterm_instantiate;
2015-07-25 wenzelm 2015-07-25 more accurate maxidx;
2015-07-25 wenzelm 2015-07-25 clarified error;
2015-07-25 wenzelm 2015-07-25 added infer_instantiate, which is meant to supersede cterm_instantiate;
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-03 wenzelm 2015-06-03 clarified context;
2015-05-31 wenzelm 2015-05-31 obsolete;
2015-05-31 wenzelm 2015-05-31 tuned;
2015-05-30 wenzelm 2015-05-30 standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
2015-05-30 wenzelm 2015-05-30 tuned;
2015-05-30 wenzelm 2015-05-30 more explicit context;
2015-05-30 wenzelm 2015-05-30 obsolete;
2015-05-30 wenzelm 2015-05-30 tuned -- more direct Thm.renamed_prop;
2015-05-03 wenzelm 2015-05-03 suppress formal sort-constraints, in accordance to norm_hhf_eqs;
2015-04-10 wenzelm 2015-04-10 tuned;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-22 wenzelm 2015-03-22 tuned;
2015-03-20 wenzelm 2015-03-20 tuned -- prepare instantiation more uniformly;
2015-03-07 wenzelm 2015-03-07 clarified Drule.gen_all: observe context more carefully;
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;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2013-06-27 wenzelm 2013-06-27 tuned signature;
2013-06-27 wenzelm 2013-06-27 tuned signature;
2013-05-29 wenzelm 2013-05-29 more precise "incremented" indication, which might be relevant in corner cases, e.g. instantiation of leading to vars with different types (which is a potential problem nonetheless);
2013-05-29 wenzelm 2013-05-29 tuned signature -- more explicit flags for low-level Thm.bicompose;
2013-05-24 wenzelm 2013-05-24 tuned signature;
2012-06-25 wenzelm 2012-06-25 eliminated obsolete swap_prems_rl -- rotate_prems usually does the job more directly;
2012-04-11 wenzelm 2012-04-11 rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
2012-03-31 wenzelm 2012-03-31 tuned signature;
2012-03-19 wenzelm 2012-03-19 moved some legacy stuff;
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2012-02-15 wenzelm 2012-02-15 discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
2012-02-14 wenzelm 2012-02-14 discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual;
2012-01-14 wenzelm 2012-01-14 tuned;
2012-01-11 wenzelm 2012-01-11 more qualified names; more antiquotations;