src/HOL/Presburger.thy
Sun, 17 Jun 2007 13:39:27 +0200 chaieb moved lemma all_not_ex to HOL.thy ; tuned proofs
Thu, 14 Jun 2007 22:59:39 +0200 chaieb Added some lemmas to default presburger simpset; tuned proofs
Thu, 14 Jun 2007 18:33:31 +0200 wenzelm tuned proofs: avoid implicit prems;
Wed, 13 Jun 2007 03:31:11 +0200 huffman removed constant int :: nat => int;
Tue, 12 Jun 2007 10:15:40 +0200 chaieb Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts
Mon, 11 Jun 2007 11:06:00 +0200 chaieb A new and cleaned up Theory for QE. for Presburger arithmetic
Tue, 05 Jun 2007 16:26:06 +0200 wenzelm tuned comments;
Thu, 31 May 2007 18:16:52 +0200 wenzelm moved Integ files to canonical place;
Thu, 31 May 2007 13:00:56 +0200 wenzelm fixed title;
Thu, 31 May 2007 12:06:31 +0200 wenzelm moved Integ files to canonical place;
Thu, 26 Apr 2007 13:33:05 +0200 haftmann cleaned up code generator setup for int
Fri, 20 Apr 2007 11:21:42 +0200 haftmann Isar definitions are now added explicitly to code theorem table
Fri, 02 Mar 2007 15:43:25 +0100 haftmann tuned code theorems for ord on integers
Sat, 06 Jan 2007 20:47:09 +0100 chaieb A few theorems on integer divisibily.
Wed, 22 Nov 2006 10:20:12 +0100 haftmann dropped eq const
Mon, 16 Oct 2006 14:07:31 +0200 haftmann moved HOL code generator setup to Code_Generator
Tue, 19 Sep 2006 15:21:58 +0200 haftmann improved numeral handling for nbe
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