src/HOL/Integ/Presburger.thy
Wed, 06 Sep 2006 13:48:02 +0200 haftmann got rid of Numeral.bin type
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Sat, 08 Jul 2006 12:54:39 +0200 wenzelm tuned;
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
Thu, 22 Sep 2005 23:56:15 +0200 nipkow renamed rules to iprover
Wed, 14 Sep 2005 17:25:52 +0200 chaieb The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
Thu, 14 Jul 2005 19:28:18 +0200 wenzelm improved oracle setup;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
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
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.
Tue, 11 May 2004 20:11:08 +0200 obua changes made due to new Ring_and_Field theory
Fri, 16 Apr 2004 04:07:10 +0200 wenzelm tuned document;
Thu, 25 Mar 2004 10:32:21 +0100 paulson new material from Avigad
Tue, 10 Feb 2004 12:02:11 +0100 paulson generic of_nat and of_int functions, and generalization of iszero
Mon, 12 Jan 2004 16:51:45 +0100 paulson Added lemmas to Ring_and_Field with slightly modified simplification rules
Wed, 03 Dec 2003 10:49:34 +0100 paulson Simplification of the development of Integers
Tue, 05 Aug 2003 17:57:39 +0200 nipkow cleaned up
Tue, 25 Mar 2003 09:47:05 +0100 berghofe New decision procedure for Presburger arithmetic.
less more (0) tip