Mon, 14 Mar 2011 14:37:41 +0100 | hoelzl | simplified definition of open_extreal | changeset | files |
Mon, 14 Mar 2011 14:37:40 +0100 | hoelzl | use case_product for extrel[2,3]_cases | changeset | files |
Mon, 14 Mar 2011 14:37:39 +0100 | hoelzl | add Extended_Reals from AFP/Lower_Semicontinuous | changeset | files |
Mon, 14 Mar 2011 14:37:37 +0100 | hoelzl | add lemmas for monotone sequences | changeset | files |
Mon, 14 Mar 2011 14:37:36 +0100 | hoelzl | add lemmas for SUP and INF | changeset | files |
Mon, 14 Mar 2011 14:37:35 +0100 | hoelzl | generalize infinite sums | changeset | files |