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 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);
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref; replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-03-29 wenzelm 2008-03-29 certify wrt. dynamic context; functional store_thm (wrt. thread data);
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2007-11-27 berghofe 2007-11-27 Better error messages for cterm_instantiate.
2007-10-11 wenzelm 2007-10-11 moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML); tuned;
2007-10-10 wenzelm 2007-10-10 improved abs_def: only abstract over outermost (unique) Vars;
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;
2007-08-24 paulson 2007-08-24 new derived rule: incr_type_indexes
2007-08-13 wenzelm 2007-08-13 SimpleSyntax.read_prop;
2007-07-29 wenzelm 2007-07-29 moved Drule.add/del/merge_rules to Thm.add/del/merge_thms; moved Drule.is_dummy_thm to Thm.is_dummy;
2007-07-27 wenzelm 2007-07-27 added dummy_thm, is_dummy_thm;
2007-07-04 wenzelm 2007-07-04 added binop_cong_rule;
2007-07-03 wenzelm 2007-07-03 tuned rotate_prems; tuned comments;
2007-06-20 paulson 2007-06-20 A more robust flexflex_unique
2007-06-19 wenzelm 2007-06-19 added with_subgoal;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-11 wenzelm 2007-05-11 proper type for fun/arg_cong_rule;
2007-05-11 wenzelm 2007-05-11 added fun/arg_cong_rule;
2007-05-10 wenzelm 2007-05-10 moved some operations to more_thm.ML and conv.ML;
2007-04-15 wenzelm 2007-04-15 moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.; Term.string_of_vname;
2007-04-02 paulson 2007-04-02 optimizing the null instantiation case
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-13 paulson 2007-02-13 COMP now performs a distinctness check on the multiple results before failing
2007-02-10 paulson 2007-02-10 Completing the bug fix from the previous update: the result of unifying type variables must be normalized WRT itself; otherwise instantiation is wrong
2007-02-08 paulson 2007-02-08 cterm_instantiate was calling a type instantiation function that works only for matching, not unification as here.