src/HOL/Integ/presburger.ML
Sat, 08 Jul 2006 12:54:41 +0200 wenzelm presburger_ss: proper context;
Fri, 17 Mar 2006 09:34:23 +0100 haftmann renamed op < <= to Orderings.less(_eq)
Fri, 10 Mar 2006 15:33:48 +0100 haftmann renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Tue, 13 Dec 2005 16:24:12 +0100 chaieb deals with Suc in mod expressions
Fri, 18 Nov 2005 07:13:58 +0100 chaieb presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
Fri, 11 Nov 2005 10:49:59 +0100 chaieb old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
Sat, 17 Sep 2005 18:11:25 +0200 wenzelm removed obsolete BasisLibrary;
Thu, 14 Jul 2005 19:28:18 +0200 wenzelm improved oracle setup;
Thu, 07 Apr 2005 09:25:33 +0200 wenzelm reverted renaming of Some/None in comments and strings;
Wed, 23 Mar 2005 12:09:18 +0100 paulson replaced bool by a new datatype "bit" for binary numerals
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 11 Oct 2004 19:36:48 +0200 berghofe Replaced the_context() by theory "Presburger" in call of invoke_oracle.
Thu, 01 Jul 2004 12:29:53 +0200 paulson new treatment of binary numerals
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Mon, 14 Jun 2004 16:46:48 +0200 chaieb Oracle corrected
Sat, 12 Jun 2004 13:50:55 +0200 chaieb An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
Sun, 06 Jun 2004 18:36:36 +0200 wenzelm avoid Args.list (lost update?);
Sat, 05 Jun 2004 18:34:06 +0200 chaieb More readable code.
Sat, 29 May 2004 15:09:47 +0200 wenzelm avoid Args.list;
Wed, 26 May 2004 19:06:09 +0200 chaieb abstraction over functions is no default any more.
Fri, 21 May 2004 21:49:45 +0200 berghofe - deleted unneeded function eta_long (now in Pure/pattern.ML
Wed, 19 May 2004 11:23:59 +0200 chaieb A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
Mon, 12 Jan 2004 16:51:45 +0100 paulson Added lemmas to Ring_and_Field with slightly modified simplification rules
Thu, 24 Jul 2003 17:52:38 +0200 berghofe Fixed two bugs:
Sat, 10 May 2003 20:52:18 +0200 berghofe - Added split_min and split_max to preprocessor
Fri, 04 Apr 2003 17:01:12 +0200 berghofe Fixed bug in eta_long.
Tue, 25 Mar 2003 09:47:05 +0100 berghofe New decision procedure for Presburger arithmetic.
less more (0) tip