Ordering is now: first by number of assumptions, second by the substitution size. Treat elim/dest rules like erule/drule would: * "elim" is now a subset of "dest" and matches on conclusion of goal and major premise against any premise of goal. Computed substitution size takes both into account. * "dest" no longer has a restriction that limits its conclusion to a var. (contributed by Raf)

addedd ID line

mentioned Ln in NEWS

fixed minor typo in comments

changed import to Ln

added a new theory; properties of ln

P.opt_locale_target;

nameless theorems: better names, flag to omit them

invents theorem names; also patches write_out_clasimp

dead code

new function trim_ends

uniform treatment of variable prefixes

corrected some typos

new droplet

Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files

tuned gen_all, forall_elim_list, implies_intr_list, standard; impose_hyps: use Thm.weaken; zero_var_indexes: use Term.zero_var_indexes_inst; Sign.typ_unify;

Sign.typ_unify; tuned;

Sign.typ_unify; Tactic.prove;

typ_match, unify: canonical argument order; added raw_match, raw_instance; proper implementation of raw_unify;

added weaken, adjust_maxidx_thm;

check_overloading replaces datatype overloading; tuned;

added add_tfreesT, add_tfrees; added bound; added zero_var_indexesT, zero_var_indexes, zero_var_indexes_subst; removed add_term_constsT; tuned;

norm_hhf_rule: Thm.adjust_maxidx_thm before Drule.gen_all; removed prove_standard, prove_multi_standard;

added add_const_constraint(_i), const_constraint; added typ_match, typ_unify;

adapted Type.typ_match; tuned;

Sign.typ_unify; Term.bound; tuned rewrite_term;

Term.bound;

print_theory: const constraints;

Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;

Sign.typ_match;

Sign.typ_unify;

fixed var index in tactic;