src/HOL/Library/Extended_Reals.thy
2011-03-14 wenzelm 2011-03-14 standardized headers;
2011-03-14 hoelzl 2011-03-14 split Extended_Reals into parts for Library and Multivariate_Analysis
2011-03-14 hoelzl 2011-03-14 lemmas about addition, SUP on countable sets and infinite sums for extreal
2011-03-14 hoelzl 2011-03-14 add infinite sums and power on extreal
2011-03-14 hoelzl 2011-03-14 introduce setsum on extreal
2011-03-14 hoelzl 2011-03-14 use abs_extreal
2011-03-14 hoelzl 2011-03-14 simplified definition of open_extreal
2011-03-14 hoelzl 2011-03-14 use case_product for extrel[2,3]_cases
2011-03-14 hoelzl 2011-03-14 add Extended_Reals from AFP/Lower_Semicontinuous