2005-08-01 wenzelm 2005-08-01 removed atless (use term_ord instead); removed (inefficient) insert_aterm; improved bound: nameless, avoid allocating new strings; tuned sort_ord/typ_ord: dict_ord; tuned abstract_over: SAME; tuned add_term_vars/frees: OrdList.insert; removed compress_type/compress_type (cf. compress.ML);
2005-08-01 wenzelm 2005-08-01 export MataSimplifier.inherit_bounds;
2005-08-01 wenzelm 2005-08-01 Compress.typ;
2005-08-01 wenzelm 2005-08-01 Compress.init_data;
2005-08-01 wenzelm 2005-08-01 nameless Term.bound;
2005-08-01 wenzelm 2005-08-01 improved bounds: nameless Term.bound, recover names for output;
2005-08-01 wenzelm 2005-08-01 tuned dict_ord;
2005-08-01 wenzelm 2005-08-01 replaced atless by term_ord;
2005-08-01 wenzelm 2005-08-01 chain_history: turned into runtime flag; added monomorphic; removed (inefficient) fast_overloading_info; Compress.typ; tuned;
2005-08-01 wenzelm 2005-08-01 compression of terms and types by sharing common subtrees;
2005-08-01 wenzelm 2005-08-01 added compress.ML;
2005-08-01 wenzelm 2005-08-01 Term.is_bound;
2005-08-01 wenzelm 2005-08-01 tuned signature;
2005-08-01 wenzelm 2005-08-01 no eq_commute;
2005-08-01 wenzelm 2005-08-01 Defs.monomorphic;
2005-08-01 wenzelm 2005-08-01 Sign.read_term;
2005-08-01 wenzelm 2005-08-01 more zcong_sym;
2005-08-01 wenzelm 2005-08-01 simprocs: Simplifier.inherit_bounds;
2005-08-01 wenzelm 2005-08-01 no eq_sym_conv; tuned;
2005-08-01 wenzelm 2005-08-01 removed read_cterm; tuned;
2005-08-01 wenzelm 2005-08-01 tuned msg;
2005-08-01 wenzelm 2005-08-01 PolyML.Compiler.printInAlphabeticalOrder := false;
2005-08-01 wenzelm 2005-08-01 polyml: use polyml-platform/version from Isabelle distribution; removed DEFS_CHAIN_HISTORY;
2005-08-01 wenzelm 2005-08-01 obsolete;
2005-08-01 obua 2005-08-01 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
2005-08-01 nipkow 2005-08-01 added map_filter lemmas
2005-08-01 kleing 2005-08-01 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)
2005-07-30 nipkow 2005-07-30 addedd ID line
2005-07-29 avigad 2005-07-29 mentioned Ln in NEWS
2005-07-29 avigad 2005-07-29 fixed minor typo in comments
2005-07-29 avigad 2005-07-29 changed import to Ln
2005-07-29 avigad 2005-07-29 added a new theory; properties of ln
2005-07-29 wenzelm 2005-07-29 P.opt_locale_target;
2005-07-29 paulson 2005-07-29 nameless theorems: better names, flag to omit them
2005-07-28 paulson 2005-07-28 invents theorem names; also patches write_out_clasimp
2005-07-28 paulson 2005-07-28 dead code
2005-07-28 paulson 2005-07-28 new function trim_ends
2005-07-28 paulson 2005-07-28 uniform treatment of variable prefixes
2005-07-28 haftmann 2005-07-28 corrected some typos
2005-07-28 paulson 2005-07-28 new droplet
2005-07-28 quigley 2005-07-28 Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
2005-07-28 wenzelm 2005-07-28 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;
2005-07-28 wenzelm 2005-07-28 Sign.typ_unify; tuned;
2005-07-28 wenzelm 2005-07-28 Sign.typ_unify; Tactic.prove;
2005-07-28 wenzelm 2005-07-28 typ_match, unify: canonical argument order; added raw_match, raw_instance; proper implementation of raw_unify;
2005-07-28 wenzelm 2005-07-28 added weaken, adjust_maxidx_thm;
2005-07-28 wenzelm 2005-07-28 check_overloading replaces datatype overloading; tuned;
2005-07-28 wenzelm 2005-07-28 added add_tfreesT, add_tfrees; added bound; added zero_var_indexesT, zero_var_indexes, zero_var_indexes_subst; removed add_term_constsT; tuned;
2005-07-28 wenzelm 2005-07-28 norm_hhf_rule: Thm.adjust_maxidx_thm before Drule.gen_all; removed prove_standard, prove_multi_standard;
2005-07-28 wenzelm 2005-07-28 added add_const_constraint(_i), const_constraint; added typ_match, typ_unify;
2005-07-28 wenzelm 2005-07-28 adapted Type.typ_match; tuned;
2005-07-28 wenzelm 2005-07-28 Sign.typ_unify; Term.bound; tuned rewrite_term;
2005-07-28 wenzelm 2005-07-28 Term.bound;
2005-07-28 wenzelm 2005-07-28 print_theory: const constraints;
2005-07-28 wenzelm 2005-07-28 Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;
2005-07-28 wenzelm 2005-07-28 Sign.typ_match;
2005-07-28 wenzelm 2005-07-28 Sign.typ_unify;
2005-07-28 wenzelm 2005-07-28 fixed var index in tactic;
2005-07-28 wenzelm 2005-07-28 proper header;
2005-07-28 wenzelm 2005-07-28 Sign.typ_instance;