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