src/HOL/Library/Extended_Reals.thy
changeset 43141 11fce8564415
parent 42950 6e5c2a3c69da
child 43138 818521a90356