| Mon, 23 May 2011 19:21:05 +0200 |
hoelzl |
move lemmas to Extended_Reals and Extended_Real_Limits
|
file |
diff |
annotate
|
| Mon, 02 May 2011 10:50:09 +0200 |
bulwahn |
fixing typo
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 16:59:37 +0100 |
wenzelm |
standardized headers;
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:47 +0100 |
hoelzl |
split Extended_Reals into parts for Library and Multivariate_Analysis
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:46 +0100 |
hoelzl |
lemmas about addition, SUP on countable sets and infinite sums for extreal
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:45 +0100 |
hoelzl |
add infinite sums and power on extreal
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:44 +0100 |
hoelzl |
introduce setsum on extreal
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:42 +0100 |
hoelzl |
use abs_extreal
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:41 +0100 |
hoelzl |
simplified definition of open_extreal
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:40 +0100 |
hoelzl |
use case_product for extrel[2,3]_cases
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:39 +0100 |
hoelzl |
add Extended_Reals from AFP/Lower_Semicontinuous
|
file |
diff |
annotate
|