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);
2007-10-10 ago improved abs_def: only abstract over outermost (unique) Vars;
2007-10-04 ago replaced literal 'a by Name.aT;
2007-08-24 ago new derived rule: incr_type_indexes
2007-08-13 ago SimpleSyntax.read_prop;
2007-07-29 ago moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-07-27 ago added dummy_thm, is_dummy_thm;
2007-07-04 ago added binop_cong_rule;
2007-07-03 ago tuned rotate_prems;
2007-06-20 ago A more robust flexflex_unique
2007-06-19 ago added with_subgoal;
2007-05-31 ago simplified/unified list fold;
2007-05-11 ago proper type for fun/arg_cong_rule;
2007-05-11 ago added fun/arg_cong_rule;
2007-05-10 ago moved some operations to more_thm.ML and conv.ML;
2007-04-15 ago moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
2007-04-14 ago cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-02 ago optimizing the null instantiation case
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-13 ago COMP now performs a distinctness check on the multiple results before failing
2007-02-10 ago Completing the bug fix from the previous update: the result of unifying type
2007-02-08 ago cterm_instantiate was calling a type instantiation function that works only for matching,