src/Provers/Arith/fast_lin_arith.ML
2006-01-19 ago setup: theory -> theory;
2006-01-04 ago removed pointless trace msg.
2005-12-02 ago introduced new map2, fold
2005-10-28 ago cleaned up nth, nth_update, nth_map and nth_string functions
2005-10-21 ago introduced functions from Pure/General/rat.ML
2005-10-18 ago Simplifier.theory_context;
2005-10-17 ago Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-09-23 ago Simplifier.inherit_bounds;
2005-09-20 ago fixed syntax for sml/nj
2005-09-20 ago Simplifier.inherit_bounds;
2005-09-20 ago slight adaptions to library changes
2005-09-12 ago introduced new-style AList operations
2005-08-07 ago moved some rat functions to library.ML
2005-07-07 ago takes & in premises apart now.
2005-06-17 ago accomodate change of TheoryDataFun;
2005-06-10 ago IntInf change
2005-05-16 ago Use of IntInf.int instead of int in most numeric simprocs; avoids
2005-05-04 ago neqE applies even if the type is not one which partakes in linear arithmetic.
2005-04-07 ago handle Option instead of OPTION;
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-09-06 ago made mult_mono_thms generic.
2004-07-08 ago adapted type of simprocs;
2004-05-29 ago avoid 'handle _' -- would cover Interrupt as well!!!
2004-04-02 ago introduced fast_arith_neq_limit
2004-02-14 ago Removed dangling exception handler
2004-02-03 ago Finally fixed the counterexample finder. Can now deal with < on real.
2004-01-25 ago Added an exception handler and error msg.
2002-09-09 ago bug in counter example finder
2002-08-23 ago for cancelling div + mod.
2002-08-13 ago Added counter example generation.
2002-08-07 ago Fixed two bugs
2002-05-30 ago Big update. Allows case splitting on ~= now (trying both < and >).
2002-05-07 ago use eq_thm_prop instead of slightly inadequate eq_thm;
2002-02-25 ago updated debugging output
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-24 ago gen_merge_lists';
2001-11-21 ago use tracing function for trace output;
2001-11-08 ago theory data: finish method;
2000-12-21 ago rational arithemtic
2000-12-18 ago towards rtional arithmetic
2000-12-01 ago Now adjusted to mixed terms involving coercions.
2000-07-24 ago avoid global references;
2000-06-16 ago tracing flag for arith_tac
2000-02-19 ago Commenst.
1999-09-23 ago Restructured lin.arith.package.
1999-09-21 ago Mod because of new solver interface.
1999-09-21 ago Added comments.
1999-09-21 ago Now distinguishes discrete from non-distrete types.
1999-01-14 ago More arith refinements.
1999-01-13 ago Simplified interface.
1999-01-12 ago Split argument structure.
1999-01-11 ago More arith simplifications.
1999-01-09 ago Added simproc.
1999-01-05 ago Small mods.
1999-01-04 ago Version 1 of linear arithmetic for nat.
1998-11-27 ago Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.