Mon, 03 Dec 2012 18:19:09 +0100 | hoelzl | weakened assumptions for lhopital_right_0 | changeset | files |
Mon, 03 Dec 2012 18:19:08 +0100 | hoelzl | tuned proof | changeset | files |
Mon, 03 Dec 2012 18:19:07 +0100 | hoelzl | add L'Hôpital's rule | changeset | files |
Mon, 03 Dec 2012 18:19:05 +0100 | hoelzl | add filterlim rules for exp and ln to infinity | changeset | files |
Mon, 03 Dec 2012 18:19:04 +0100 | hoelzl | add filterlim rules for inverse and at_infinity | changeset | files |
Mon, 03 Dec 2012 18:19:02 +0100 | hoelzl | add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image | changeset | files |
Mon, 03 Dec 2012 18:19:01 +0100 | hoelzl | add filterlim rules for unary minus and inverse | changeset | files |
Mon, 03 Dec 2012 18:18:59 +0100 | hoelzl | rename filter_lim to filterlim to be consistent with filtermap | changeset | files |