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 |