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.