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