src/Pure/drule.ML
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;
2010-02-19 wenzelm 2010-02-19 moved ancient Drule.get_def to OldGoals.get_def;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-21 wenzelm 2009-11-21 explicitly mark some legacy freeze operations;
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-02 wenzelm 2009-11-02 modernized structure Simple_Syntax;
2009-10-28 wenzelm 2009-10-28 Drule.store: proper binding; conceal internal bindings;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-17 wenzelm 2009-10-17 legacy Drule.standard is no longer pervasive;
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-07-02 wenzelm 2009-07-02 renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
2009-03-16 wenzelm 2009-03-16 refined is_norm_hhf: reject beta-redexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract;
2009-03-07 wenzelm 2009-03-07 moved Thm.def_name(_optional) to more_thm.ML; moved old-style Thm.get_def to Drule.get_def;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2009-01-04 wenzelm 2009-01-04 added comp_no_flatten;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-10-31 berghofe 2008-10-31 Theorem "_" is now stored with open derivation.
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-10-16 wenzelm 2008-10-16 added rules for sort_constraint, include in norm_hhf_eqs; tuned;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-06-23 wenzelm 2008-06-23 Logic.implies;
2008-06-19 wenzelm 2008-06-19 moved add_used to Isar/rule_insts.ML;
2008-06-16 wenzelm 2008-06-16 removed obsolete global read_insts/read_instantiate (cf. Isar/rule_insts.ML);
2008-06-11 wenzelm 2008-06-11 qualified types_sorts, read_insts etc.;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-15 wenzelm 2008-04-15 Thm.forall_elim_var(s);