| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Tue, 17 Jan 2012 16:30:54 +0100 |
huffman |
factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 17:21:29 +0100 |
huffman |
tendsto lemmas for ln and powr
|
file |
diff |
annotate
|
| Sun, 30 Oct 2011 09:42:13 +0100 |
huffman |
removed ad-hoc simp rules sin_cos_eq[symmetric], minus_sin_cos_eq[symmetric], cos_sin_eq[symmetric]
|
file |
diff |
annotate
|
| Sun, 30 Oct 2011 09:07:02 +0100 |
huffman |
extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 10:30:00 -0700 |
huffman |
simplify proof of tan_half, removing unused assumptions
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 09:56:09 -0700 |
huffman |
convert some proofs to Isar-style
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 22:30:25 -0700 |
huffman |
add lemmas about arctan;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 18:06:02 -0700 |
huffman |
convert lemma cos_total to Isar-style proof
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 17:45:37 -0700 |
huffman |
convert lemma cos_is_zero to Isar-style
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 17:00:56 -0700 |
huffman |
convert lemma sin_gt_zero to Isar style;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 16:26:57 -0700 |
huffman |
modify lemma sums_group, and shorten proofs that use it
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 16:07:40 -0700 |
huffman |
generalize some lemmas
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 12:19:04 -0700 |
huffman |
add lemmas cos_arctan and sin_arctan
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 09:49:45 -0700 |
huffman |
remove redundant lemmas about LIMSEQ
|
file |
diff |
annotate
|
| Sun, 28 Aug 2011 09:20:12 -0700 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 18:42:41 -0700 |
huffman |
move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 18:08:05 -0700 |
huffman |
remove unused lemma DERIV_sin_add
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 18:06:27 -0700 |
huffman |
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 17:59:19 -0700 |
huffman |
remove redundant lemma exp_ln_eq in favor of ln_unique
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 14:17:28 -0700 |
huffman |
Transcendental.thy: add tendsto_intros lemmas;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 10:46:54 -0700 |
huffman |
Transcendental.thy: remove several unused lemmas and simplify some proofs
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 08:40:15 -0700 |
huffman |
remove unused lemmas
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 07:45:22 -0700 |
huffman |
remove some redundant simp rules
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 19:53:03 -0700 |
huffman |
optimize some proofs
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
| Tue, 31 May 2011 21:33:49 +0200 |
hoelzl |
use divide instead of inverse for the derivative of ln
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:35 +0100 |
hoelzl |
generalize infinite sums
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:17:13 +0200 |
haftmann |
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
|
file |
diff |
annotate
|