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