src/HOL/Library/Extended_Reals.thy
changeset 43704 47b0be18ccbe
parent 43138 818521a90356