| Wed, 04 Mar 2009 17:12:23 -0800 |
huffman |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
file |
diff |
annotate
|
| Tue, 24 Feb 2009 11:12:58 -0800 |
huffman |
make more proofs work whether or not One_nat_def is a simp rule
|
file |
diff |
annotate
|
| Thu, 05 Feb 2009 11:34:42 +0100 |
hoelzl |
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
|
file |
diff |
annotate
|
| Fri, 30 Jan 2009 12:48:57 +0000 |
chaieb |
Added real related theorems from Fact.thy
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Wed, 24 Dec 2008 13:29:49 -0800 |
huffman |
clean up lemmas about ln
|
file |
diff |
annotate
|
| Wed, 24 Dec 2008 13:16:26 -0800 |
huffman |
clean up lemmas about exp
|
file |
diff |
annotate
|
| Wed, 24 Dec 2008 08:40:16 -0800 |
huffman |
rearranged subsections; cleaned up some proofs
|
file |
diff |
annotate
|
| Wed, 24 Dec 2008 08:16:45 -0800 |
huffman |
move theorems about limits from Transcendental.thy to Deriv.thy
|
file |
diff |
annotate
|
| Wed, 24 Dec 2008 08:06:27 -0800 |
huffman |
cleaned up some proofs; removed redundant simp rules
|
file |
diff |
annotate
|
| Tue, 23 Dec 2008 15:02:30 -0800 |
huffman |
move sin and cos to their own subsection
|
file |
diff |
annotate
|
| Tue, 23 Dec 2008 14:31:47 -0800 |
huffman |
clean up some proofs; remove unused lemmas
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
| base
|