src/Pure/drule.ML
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;
2011-11-05 wenzelm 2011-11-05 tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
2011-11-05 wenzelm 2011-11-05 misc tuning and modernization;
2011-10-16 wenzelm 2011-10-16 added Term.dummy_pattern conveniences;
2011-08-10 wenzelm 2011-08-10 avoid OldTerm operations -- with subtle changes of semantics;
2011-06-27 wenzelm 2011-06-27 old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
2011-06-09 wenzelm 2011-06-09 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-06-09 wenzelm 2011-06-09 clarified special incr_type_indexes;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-04-23 wenzelm 2011-04-23 hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-25 wenzelm 2010-08-25 structure Thm: less pervasive names;
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-03 wenzelm 2010-05-03 renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-04-25 wenzelm 2010-04-25 renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp; less pervasive names;
2010-03-27 wenzelm 2010-03-27 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML); discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def; modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
2010-03-22 wenzelm 2010-03-22 eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
2010-03-22 wenzelm 2010-03-22 replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;