| Tue, 05 Jun 2007 19:19:30 +0200 |
haftmann |
tuned integers
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 16:26:06 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 13:00:56 +0200 |
wenzelm |
fixed title;
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:40 +0200 |
haftmann |
canonical prefixing of class constants
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:33:12 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 18 Dec 2006 08:21:29 +0100 |
haftmann |
introduced abstract view on number expressions in hologic.ML
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 15:45:31 +0100 |
haftmann |
introduced mk/dest_numeral/number for mk/dest_binum etc.
|
file |
diff |
annotate
|
| Sat, 18 Nov 2006 00:20:24 +0100 |
haftmann |
dvd_def now with object equality
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 17:07:26 +0200 |
haftmann |
slight cleanup
|
file |
diff |
annotate
|
| Tue, 26 Sep 2006 13:34:16 +0200 |
haftmann |
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 14:28:47 +0200 |
haftmann |
hid succ, pred in Numeral.thy
|
file |
diff |
annotate
|
| Tue, 25 Jul 2006 21:18:00 +0200 |
wenzelm |
renamed Term.variant_abs to Syntax.variant_abs;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 12:11:56 +0200 |
paulson |
renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 09:34:23 +0100 |
haftmann |
renamed op < <= to Orderings.less(_eq)
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 15:33:48 +0100 |
haftmann |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 16:17:34 +0200 |
haftmann |
introduced AList module in favor of assoc etc.
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 16:38:35 +0200 |
haftmann |
introduced AList module
|
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:19 +0200 |
wenzelm |
improved oracle setup;
|
file |
diff |
annotate
|
| Wed, 15 Jun 2005 13:46:00 +0200 |
chaieb |
int -> IntInf.int
|
file |
diff |
annotate
|
| Tue, 14 Jun 2005 09:46:35 +0200 |
chaieb |
int --> IntInt.int
|
file |
diff |
annotate
|
| Mon, 06 Jun 2005 13:43:39 +0200 |
chaieb |
Some error messages have been eliminated as suggested by Tobias Nipkow
|
file |
diff |
annotate
|
| Mon, 16 May 2005 10:29:15 +0200 |
paulson |
Use of IntInf.int instead of int in most numeric simprocs; avoids
|
file |
diff |
annotate
|
| Wed, 27 Apr 2005 11:49:20 +0200 |
chaieb |
bug in plusinf and mininf for the oracle fixed.
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 09:25:33 +0200 |
wenzelm |
reverted renaming of Some/None in comments and strings;
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Thu, 28 Oct 2004 11:58:22 +0200 |
chaieb |
efficienty improvement
|
file |
diff |
annotate
|
| Mon, 30 Aug 2004 12:01:52 +0200 |
chaieb |
m dvd t where m is non numeral is now catched!
|
file |
diff |
annotate
|
| Wed, 04 Aug 2004 17:43:55 +0200 |
chaieb |
oracle corrected
|
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
|
| 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.
|
file |
diff |
annotate
|
| Sat, 05 Jun 2004 18:34:06 +0200 |
chaieb |
More readable code.
|
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, 25 Mar 2003 09:47:05 +0100 |
berghofe |
New decision procedure for Presburger arithmetic.
|
file |
diff |
annotate
|