| Sat, 20 Oct 2007 12:09:33 +0200 |
chaieb |
fixed proofs
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 10:24:49 +0200 |
paulson |
metis calls
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 23:24:10 +0200 |
wenzelm |
tuned ML setup;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 07:58:50 +0200 |
huffman |
remove simp attribute from lemma_STAR theorems
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:02:16 +0200 |
huffman |
replace (- 1) with -1
|
file |
diff |
annotate
|
| Tue, 22 May 2007 07:29:49 +0200 |
huffman |
rename lemmas LIM_ident, isCont_ident, DERIV_ident
|
file |
diff |
annotate
|
| Thu, 17 May 2007 00:45:27 +0200 |
huffman |
cleaned up proof of Maclaurin_sin_bound
|
file |
diff |
annotate
|
| Wed, 16 May 2007 23:03:45 +0200 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 04:31:34 +0100 |
huffman |
add type annotation
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 17:10:55 +0200 |
huffman |
add type annotations for DERIV
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| Wed, 27 Jul 2005 11:28:18 +0200 |
paulson |
removed the dependence on abs_mult
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 19:49:07 +0200 |
avigad |
Additions to the Real (and Hyperreal) libraries:
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 17:56:03 +0200 |
avigad |
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
|
file |
diff |
annotate
|