Sat, 24 Apr 2010 13:31:52 -0700 |
huffman |
document generation for Multivariate_Analysis
|
file |
diff |
annotate
|
Fri, 23 Apr 2010 23:33:48 +0200 |
wenzelm |
eliminated spurious schematic statements;
|
file |
diff |
annotate
|
Wed, 21 Apr 2010 10:44:44 +0200 |
hoelzl |
Only use provided SMT-certificates in HOL-Multivariate_Analysis.
|
file |
diff |
annotate
|
Tue, 20 Apr 2010 14:07:52 +0200 |
himmelma |
Translated remaining theorems about integration from HOL light.
|
file |
diff |
annotate
|
Wed, 07 Apr 2010 19:48:58 +0200 |
boehmes |
renamed "smt_record" to "smt_fixed" (somewhat more expressive) and inverted its semantics
|
file |
diff |
annotate
|
Wed, 24 Mar 2010 14:03:52 +0100 |
boehmes |
inhibit invokation of external SMT solver
|
file |
diff |
annotate
|
Tue, 09 Mar 2010 15:42:23 +0100 |
himmelma |
reset smt_certificates
|
file |
diff |
annotate
|
Tue, 09 Mar 2010 15:39:26 +0100 |
himmelma |
added lemmas
|
file |
diff |
annotate
|
Tue, 02 Mar 2010 09:57:49 +0100 |
himmelma |
the ordering on real^1 is linear
|
file |
diff |
annotate
|
Mon, 22 Feb 2010 20:41:49 +0100 |
hoelzl |
Replaced Integration by Multivariate-Analysis/Real_Integration
|
file |
diff |
annotate
| base
|
Wed, 17 Feb 2010 18:33:45 +0100 |
himmelma |
Added integration to Multivariate-Analysis (upto FTC)
|
file |
diff |
annotate
|