src/HOL/Integ/cooper_dec.ML
2005-06-15 chaieb 2005-06-15 int -> IntInf.int
2005-06-14 chaieb 2005-06-14 int --> IntInt.int
2005-06-06 chaieb 2005-06-06 Some error messages have been eliminated as suggested by Tobias Nipkow
2005-05-16 paulson 2005-05-16 Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
2005-04-27 chaieb 2005-04-27 bug in plusinf and mininf for the oracle fixed.
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-10-28 chaieb 2004-10-28 efficienty improvement Heuristic is now the same as for the proof-generating alg.
2004-08-30 chaieb 2004-08-30 m dvd t where m is non numeral is now catched!
2004-08-04 chaieb 2004-08-04 oracle corrected
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-14 chaieb 2004-06-14 Oracle corrected
2004-06-12 chaieb 2004-06-12 An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
2004-06-05 chaieb 2004-06-05 More readable code.
2004-05-19 chaieb 2004-05-19 A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
2003-03-25 berghofe 2003-03-25 New decision procedure for Presburger arithmetic.