src/HOL/Integ/cooper_proof.ML
2005-06-14 chaieb 2005-06-14 int --> IntInt.int
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-08-30 chaieb 2004-08-30 corrected
2004-08-30 chaieb 2004-08-30 m dvd t where m is non numeral is now catched!
2004-08-06 chaieb 2004-08-06 *** empty log message ***
2004-08-06 chaieb 2004-08-06 proof_of_evalc corrected;
2004-08-04 chaieb 2004-08-04 oracle corrected
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
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.
2004-03-24 paulson 2004-03-24 streamlined treatment of quotients for the integers
2003-11-18 paulson 2003-11-18 conversion of ML to Isar scripts
2003-08-05 nipkow 2003-08-05 cleaned up
2003-04-08 berghofe 2003-04-08 Fixed bug in adjustcoeffeq_wp.
2003-03-25 berghofe 2003-03-25 New decision procedure for Presburger arithmetic.