src/Provers/Arith/fast_lin_arith.ML
2001-11-24 wenzelm 2001-11-24 gen_merge_lists';
2001-11-21 wenzelm 2001-11-21 use tracing function for trace output;
2001-11-08 wenzelm 2001-11-08 theory data: finish method;
2000-12-21 nipkow 2000-12-21 rational arithemtic
2000-12-18 nipkow 2000-12-18 towards rtional arithmetic
2000-12-01 nipkow 2000-12-01 Now adjusted to mixed terms involving coercions.
2000-07-24 wenzelm 2000-07-24 avoid global references;
2000-06-16 paulson 2000-06-16 tracing flag for arith_tac
2000-02-19 nipkow 2000-02-19 Commenst.
1999-09-23 nipkow 1999-09-23 Restructured lin.arith.package.
1999-09-21 nipkow 1999-09-21 Mod because of new solver interface.
1999-09-21 nipkow 1999-09-21 Added comments.
1999-09-21 nipkow 1999-09-21 Now distinguishes discrete from non-distrete types.
1999-01-14 nipkow 1999-01-14 More arith refinements.
1999-01-13 nipkow 1999-01-13 Simplified interface.
1999-01-12 nipkow 1999-01-12 Split argument structure.
1999-01-11 nipkow 1999-01-11 More arith simplifications.
1999-01-09 nipkow 1999-01-09 Added simproc.
1999-01-05 nipkow 1999-01-05 Small mods.
1999-01-04 nipkow 1999-01-04 Version 1 of linear arithmetic for nat.
1998-11-27 nipkow 1998-11-27 Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.