no eq_commute;

Defs.monomorphic;

Sign.read_term;

more zcong_sym;

simprocs: Simplifier.inherit_bounds;

no eq_sym_conv; tuned;

removed read_cterm; tuned;

tuned msg;

PolyML.Compiler.printInAlphabeticalOrder := false;

polyml: use polyml-platform/version from Isabelle distribution; removed DEFS_CHAIN_HISTORY;

obsolete;

1. changed configuration variables for linear programming (Cplex_tools): LP_SOLVER is either CPLEX or GLPK CPLEX_PATH is the path to the cplex binary GLPK_PATH is the path to the glpk binary The change makes it possible to switch between glpk and cplex at runtime. 2. moved conflicting list theories out of Library.thy into ROOT.ML

added map_filter lemmas

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;