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