| Tue, 18 Sep 2007 16:08:08 +0200 |
wenzelm |
reactivated tests in smlnj;
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 15:28:11 +0200 |
wenzelm |
simultaneous use_thys;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 15:42:07 +0200 |
wenzelm |
replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
|
file |
diff |
annotate
|
| Sun, 10 Jun 2007 21:06:59 +0200 |
wenzelm |
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 20:44:12 +0200 |
chaieb |
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
|
file |
diff |
annotate
|
| Tue, 16 May 2006 13:01:22 +0200 |
wenzelm |
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
|
file |
diff |
annotate
|
| Wed, 26 Apr 2006 07:01:33 +0200 |
kleing |
moved arithmetic series to geometric series in SetInterval
|
file |
diff |
annotate
|
| Fri, 07 Apr 2006 12:48:10 +0200 |
kleing |
remame ASeries to Arithmetic_Series
|
file |
diff |
annotate
|
| Sun, 19 Feb 2006 22:40:18 +0100 |
kleing |
fixed document
|
file |
diff |
annotate
|
| Sun, 19 Feb 2006 22:12:30 +0100 |
kleing |
* denumerability of rationals by Benjamin Porter, based on NatPair (by Stefan Richter)
|
file |
diff |
annotate
|
| Sun, 19 Feb 2006 13:21:32 +0100 |
kleing |
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:35 +0200 |
wenzelm |
added Complex/ex/BigO_Complex.thy;
|
file |
diff |
annotate
|
| Tue, 06 May 2003 17:45:54 +0200 |
paulson |
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
|
file |
diff |
annotate
|
| Mon, 05 May 2003 18:22:31 +0200 |
paulson |
new session Complex for the complex numbers
|
file |
diff |
annotate
|