src/Provers/Arith/fast_lin_arith.ML
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-03-22 boehmes 2010-03-22 removed warning_count (known causes for warnings have been resolved)
2010-03-22 boehmes 2010-03-22 removed e-mail address from error message
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2010-03-09 hoelzl 2010-03-09 Use same order of neq-elimination as in proof search.
2010-02-19 wenzelm 2010-02-19 Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 eliminated some old folds;
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-19 wenzelm 2009-10-19 uniform use of Integer.add/mult/sum/prod;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-30 wenzelm 2009-07-30 qualified Subgoal.FOCUS;
2009-07-26 wenzelm 2009-07-26 replaced old METAHYPS by FOCUS;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-10 haftmann 2009-07-10 dropped find_index_eq
2009-06-15 haftmann 2009-06-15 made SML/NJ happy
2009-06-09 boehmes 2009-06-09 tuned
2009-06-08 boehmes 2009-06-08 fast_lin_arith uses proper multiplication instead of unfolding to additions
2009-05-11 haftmann 2009-05-11 mk_number replaces number_of
2009-03-23 haftmann 2009-03-23 tuned error messages
2009-03-10 webertj 2009-03-10 Instead of giving up entirely, arith now ignores all inequalities when there are too many.
2008-05-29 wenzelm 2008-05-29 added warning_count for issued reconstruction failure messages (limit 10); less nesting of let expressions;
2008-05-18 wenzelm 2008-05-18 renamed type decompT to decomp; refute: proper context for trace_ex; some attempts to improve readability;
2008-05-07 berghofe 2008-05-07 Lookup and union operations on terms are now modulo eta conversion.
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-08-01 wenzelm 2007-08-01 simplified internal Config interface;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context; turned fast_arith_split/neq_limit into configuration options; tuned signatures; misc cleanup;
2007-07-29 wenzelm 2007-07-29 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-07-05 wenzelm 2007-07-05 avoid polymorphic equality;
2007-06-29 haftmann 2007-06-29 tuned arithmetic modules
2007-06-09 wenzelm 2007-06-09 simplified type integer;
2007-06-05 haftmann 2007-06-05 tuned integers
2007-06-02 webertj 2007-06-02 cosmetic
2007-06-01 webertj 2007-06-01 additional tracing information
2007-06-01 webertj 2007-06-01 fixed handling of meta-logic propositions
2007-05-21 haftmann 2007-05-21 tuned
2007-05-19 haftmann 2007-05-19 dropped nonsense comment
2007-05-13 haftmann 2007-05-13 tuned
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2006-10-31 haftmann 2006-10-31 dropped nth_update
2006-08-30 webertj 2006-08-30 lin_arith_prover: splitting reverted because of performance loss
2006-08-02 webertj 2006-08-02 type annotations fixed (IntInf.int, to make SML/NJ happy)
2006-08-01 webertj 2006-08-01 possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
2006-07-31 webertj 2006-07-31 code reformatted
2006-07-29 webertj 2006-07-29 lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-05-11 wenzelm 2006-05-11 tuned;
2006-04-29 wenzelm 2006-04-29 tuned;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-03-24 berghofe 2006-03-24 Removed occurrences of makestring, which does not exist in SML/NJ.
2006-03-22 webertj 2006-03-22 comment fixed
2006-03-22 webertj 2006-03-22 comment for conjI added
2006-02-15 wenzelm 2006-02-15 counter example: avoid vacuous trace;