| Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 23:49:26 +0200 |
huffman |
section headings
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 20:48:47 +0200 |
wenzelm |
moved Presburger setup back to Presburger.thy;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 15:42:14 +0200 |
wenzelm |
adapted tool setup;
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 17:28:55 +0200 |
huffman |
remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 05:06:56 +0200 |
huffman |
section headings
|
file |
diff |
annotate
|
| Sun, 17 Jun 2007 13:39:27 +0200 |
chaieb |
moved lemma all_not_ex to HOL.thy ; tuned proofs
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 22:59:39 +0200 |
chaieb |
Added some lemmas to default presburger simpset; tuned proofs
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 03:31:11 +0200 |
huffman |
removed constant int :: nat => int;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 11:06:00 +0200 |
chaieb |
A new and cleaned up Theory for QE. for Presburger arithmetic
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 16:26:06 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:16:52 +0200 |
wenzelm |
moved Integ files to canonical place;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 13:00:56 +0200 |
wenzelm |
fixed title;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 12:06:31 +0200 |
wenzelm |
moved Integ files to canonical place;
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:33:05 +0200 |
haftmann |
cleaned up code generator setup for int
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Fri, 02 Mar 2007 15:43:25 +0100 |
haftmann |
tuned code theorems for ord on integers
|
file |
diff |
annotate
|
| Sat, 06 Jan 2007 20:47:09 +0100 |
chaieb |
A few theorems on integer divisibily.
|
file |
diff |
annotate
|
| Wed, 22 Nov 2006 10:20:12 +0100 |
haftmann |
dropped eq const
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:21:58 +0200 |
haftmann |
improved numeral handling for nbe
|
file |
diff |
annotate
|
| Wed, 06 Sep 2006 13:48:02 +0200 |
haftmann |
got rid of Numeral.bin type
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 23:56:15 +0200 |
nipkow |
renamed rules to iprover
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:18 +0200 |
wenzelm |
improved oracle setup;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Thu, 01 Jul 2004 12:29:53 +0200 |
paulson |
new treatment of binary numerals
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Mon, 14 Jun 2004 16:46:48 +0200 |
chaieb |
Oracle corrected
|
file |
diff |
annotate
|
| 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.
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 04:07:10 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Thu, 25 Mar 2004 10:32:21 +0100 |
paulson |
new material from Avigad
|
file |
diff |
annotate
|
| Tue, 10 Feb 2004 12:02:11 +0100 |
paulson |
generic of_nat and of_int functions, and generalization of iszero
|
file |
diff |
annotate
|
| Mon, 12 Jan 2004 16:51:45 +0100 |
paulson |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file |
diff |
annotate
|
| Wed, 03 Dec 2003 10:49:34 +0100 |
paulson |
Simplification of the development of Integers
|
file |
diff |
annotate
|
| Tue, 05 Aug 2003 17:57:39 +0200 |
nipkow |
cleaned up
|
file |
diff |
annotate
|
| Tue, 25 Mar 2003 09:47:05 +0100 |
berghofe |
New decision procedure for Presburger arithmetic.
|
file |
diff |
annotate
|