| 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
|