2012-06-25 ago eliminated obsolete swap_prems_rl -- rotate_prems usually does the job more directly;
2012-04-11 ago rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
2012-03-31 ago tuned signature;
2012-03-19 ago moved some legacy stuff;
2012-02-15 ago 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 ago 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 ago discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual;
2012-01-14 ago tuned;
2012-01-11 ago more qualified names;
2011-11-05 ago tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
2011-11-05 ago misc tuning and modernization;
2011-10-16 ago added Term.dummy_pattern conveniences;
2011-08-10 ago avoid OldTerm operations -- with subtle changes of semantics;
2011-06-27 ago old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
2011-06-09 ago renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-06-09 ago clarified special incr_type_indexes;
2011-06-09 ago discontinued Name.variant to emphasize that this is old-style / indirect;
2011-04-23 ago hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
2010-11-26 ago make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-25 ago structure Thm: less pervasive names;
2010-05-15 ago less pervasive names from structure Thm;
2010-05-03 ago renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-04-25 ago renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
2010-03-27 ago moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
2010-03-22 ago 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 ago replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-19 ago moved ancient Drule.get_def to OldGoals.get_def;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-21 ago explicitly mark some legacy freeze operations;
2009-11-12 ago eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-02 ago modernized structure Simple_Syntax;
2009-10-28 ago proper binding;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-17 ago legacy Drule.standard is no longer pervasive;
2009-07-09 ago renamed structure TermSubst to Term_Subst;
2009-07-06 ago structure Thm: less pervasive names;
2009-07-02 ago renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
2009-03-16 ago 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 ago moved Thm.def_name(_optional) to more_thm.ML;
2009-01-21 ago binding replaces bstring
2009-01-04 ago added comp_no_flatten;
2008-12-31 ago moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 ago moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-10-31 ago Theorem "_" is now stored with open derivation.
2008-10-23 ago renamed Thm.get_axiom_i to Thm.axiom;
2008-10-16 ago added rules for sort_constraint, include in norm_hhf_eqs;
2008-08-14 ago moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-06-23 ago Logic.implies;
2008-06-19 ago moved add_used to Isar/rule_insts.ML;
2008-06-16 ago removed obsolete global read_insts/read_instantiate (cf. Isar/rule_insts.ML);
2008-06-11 ago qualified types_sorts, read_insts etc.;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-04-15 ago Thm.forall_elim_var(s);
2008-04-12 ago rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-29 ago certify wrt. dynamic context;
2008-03-27 ago eliminated theory ProtoPure;
2007-11-27 ago Better error messages for cterm_instantiate.
2007-10-11 ago moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);