src/HOL/Library/Extended_Reals.thy
changeset 43918 6ca79a354c51
parent 43138 818521a90356