src/HOL/Library/Extended_Reals.thy
changeset 43244 db041e88a805
parent 43138 818521a90356