| Mon, 03 Dec 2012 20:55:32 +0100 | blanchet | tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments) | changeset | files |
| Mon, 03 Dec 2012 20:43:40 +0100 | wenzelm | some notes on the Isabelle component repository at TUM; | changeset | files |
| Mon, 03 Dec 2012 18:19:12 +0100 | hoelzl | use filterlim in Lim and SEQ; tuned proofs | changeset | files |
| Mon, 03 Dec 2012 18:19:11 +0100 | hoelzl | conversion rules for at, at_left and at_right; applied to l'Hopital's rules. | changeset | files |
| 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 |