| Fri, 17 Mar 2006 09:34:23 +0100 |
haftmann |
renamed op < <= to Orderings.less(_eq)
|
file |
diff |
annotate
|
| Sat, 11 Mar 2006 21:23:10 +0100 |
wenzelm |
got rid of type Sign.sg;
|
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, 25 Oct 2005 18:18:49 +0200 |
wenzelm |
avoid legacy goals;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:38 +0200 |
wenzelm |
OldGoals;
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 16:38:35 +0200 |
haftmann |
introduced AList module
|
file |
diff |
annotate
|
| Tue, 14 Jun 2005 09:46:35 +0200 |
chaieb |
int --> IntInt.int
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 09:25:33 +0200 |
wenzelm |
reverted renaming of Some/None in comments and strings;
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 30 Aug 2004 14:40:18 +0200 |
chaieb |
corrected
|
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
|
| Fri, 06 Aug 2004 17:29:24 +0200 |
chaieb |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 06 Aug 2004 17:19:50 +0200 |
chaieb |
proof_of_evalc corrected;
|
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
|
| 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
|
| Wed, 24 Mar 2004 10:50:29 +0100 |
paulson |
streamlined treatment of quotients for the integers
|
file |
diff |
annotate
|
| Tue, 18 Nov 2003 11:01:52 +0100 |
paulson |
conversion of ML to Isar scripts
|
file |
diff |
annotate
|
| Tue, 05 Aug 2003 17:57:39 +0200 |
nipkow |
cleaned up
|
file |
diff |
annotate
|
| Tue, 08 Apr 2003 09:44:21 +0200 |
berghofe |
Fixed bug in adjustcoeffeq_wp.
|
file |
diff |
annotate
|
| Tue, 25 Mar 2003 09:47:05 +0100 |
berghofe |
New decision procedure for Presburger arithmetic.
|
file |
diff |
annotate
|