| Tue, 04 Dec 2012 18:00:31 +0100 |
hoelzl |
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:18:59 +0100 |
hoelzl |
rename filter_lim to filterlim to be consistent with filtermap
|
file |
diff |
annotate
|
| Tue, 27 Nov 2012 19:31:11 +0100 |
hoelzl |
introduce filter_lim as a generatlization of tendsto
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 14:29:18 +0200 |
hoelzl |
add powr_inj
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 14:29:17 +0200 |
hoelzl |
add lemmas to rewrite powr to power
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 14:29:16 +0200 |
hoelzl |
add lemmas to compare log with 0 and 1
|
file |
diff |
annotate
|
| Mon, 19 Dec 2011 14:41:08 +0100 |
noschinl |
add lemmas
|
file |
diff |
annotate
|
| Mon, 19 Dec 2011 13:58:54 +0100 |
hoelzl |
isarfied proof; add log to DERIV_intros
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 17:21:29 +0100 |
huffman |
tendsto lemmas for ln and powr
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 15:55:39 +0100 |
noschinl |
add lemmas about limits
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 17:47:43 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
| Tue, 20 Apr 2010 17:58:34 +0200 |
hoelzl |
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
|
file |
diff |
annotate
|
| Mon, 16 Nov 2009 14:32:12 +0000 |
paulson |
A few more lemmas from Jeremy
|
file |
diff |
annotate
|
| Thu, 28 May 2009 22:57:17 -0700 |
huffman |
generalize constants in SEQ.thy to class metric_space
|
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
|