src/HOL/Presburger.thy
Sun, 22 Mar 2009 20:46:12 +0100 haftmann moved import of module qelim to theory Presburger
Mon, 16 Mar 2009 18:24:30 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Fri, 20 Feb 2009 23:46:03 +0100 nipkow Removed redundant lemmas
Fri, 20 Feb 2009 20:50:49 +0100 nipkow removed subsumed lemmas
Mon, 02 Feb 2009 13:56:22 +0100 haftmann dropped Id
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Wed, 03 Dec 2008 21:50:36 -0800 huffman enable eq_bin_simps for simplifying equalities on numerals
Mon, 29 Sep 2008 12:31:59 +0200 haftmann clarified dependencies between arith tools
Thu, 18 Sep 2008 19:39:44 +0200 wenzelm simplified oracle interface;
Mon, 21 Jul 2008 13:36:59 +0200 chaieb Tuned and simplified proofs
Fri, 18 Jul 2008 18:25:53 +0200 haftmann moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
Fri, 11 Jul 2008 09:02:22 +0200 haftmann separate class dvd for divisibility predicate
Wed, 02 Apr 2008 15:58:27 +0200 haftmann moved some code lemmas for Numerals to other theories
Wed, 27 Feb 2008 14:39:50 +0100 chaieb loads Tools/Qelim/qelim.ML
Sun, 17 Feb 2008 06:49:53 +0100 huffman New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
Sat, 16 Feb 2008 02:01:13 +0100 huffman added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Tue, 30 Oct 2007 08:45:54 +0100 haftmann continued localization
Fri, 12 Oct 2007 08:20:46 +0200 haftmann class div inherits from class times
Wed, 22 Aug 2007 17:13:42 +0200 chaieb tuned;
Tue, 31 Jul 2007 19:40:25 +0200 wenzelm proper context for cooper_tac within arith;
Tue, 31 Jul 2007 00:56:26 +0200 wenzelm arith method setup: proper context;
Thu, 19 Jul 2007 21:47:43 +0200 haftmann code lemma for of_int
Tue, 10 Jul 2007 09:23:11 +0200 haftmann moved lemma zdvd_period here
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
Thu, 21 Jun 2007 23:49:26 +0200 huffman section headings
Thu, 21 Jun 2007 20:48:47 +0200 wenzelm moved Presburger setup back to Presburger.thy;
Thu, 21 Jun 2007 15:42:14 +0200 wenzelm adapted tool setup;
Wed, 20 Jun 2007 17:28:55 +0200 huffman remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
Wed, 20 Jun 2007 05:06:56 +0200 huffman section headings
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.
less more (0) -60 tip