2006-03-17 haftmann 2006-03-17 renamed op < <= to Orderings.less(_eq)
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.minus HOL.times etc.
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-12-13 chaieb 2005-12-13 deals with Suc in mod expressions
2005-11-18 chaieb 2005-11-18 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
2005-11-11 chaieb 2005-11-11 old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
2005-09-17 wenzelm 2005-09-17 removed obsolete BasisLibrary;
2005-07-14 wenzelm 2005-07-14 improved oracle setup;
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-03-23 paulson 2005-03-23 replaced bool by a new datatype "bit" for binary numerals
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-11 berghofe 2004-10-11 Replaced the_context() by theory "Presburger" in call of invoke_oracle.
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
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-06 wenzelm 2004-06-06 avoid Args.list (lost update?);
2004-06-05 chaieb 2004-06-05 More readable code.
2004-05-29 wenzelm 2004-05-29 avoid Args.list;
2004-05-26 chaieb 2004-05-26 abstraction over functions is no default any more.
2004-05-21 berghofe 2004-05-21 - deleted unneeded function eta_long (now in Pure/pattern.ML - added HOL.min / HOL.max to allowed consts again - added final simplification step with presburger_ss to preprocessor again
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-01-12 paulson 2004-01-12 Added lemmas to Ring_and_Field with slightly modified simplification rules Deleted some little-used integer theorems, replacing them by the generic ones in Ring_and_Field Consolidated integer powers
2003-07-24 berghofe 2003-07-24 Fixed two bugs: - presburger_tac now calls ObjectLogic.atomize_tac first to avoid failure when premises contain meta-level quantifiers or implications - The preprocessor now also filters out premises containing variables that are not of type int or nat.
2003-05-10 berghofe 2003-05-10 - Added split_min and split_max to preprocessor - Moved eta_long to Pure/pattern.ML
2003-04-04 berghofe 2003-04-04 Fixed bug in eta_long.
2003-03-25 berghofe 2003-03-25 New decision procedure for Presburger arithmetic.