src/HOL/Library/Extended_Reals.thy
changeset 42676 8724f20bf69c
parent 42600 604661fb94eb
child 42950 6e5c2a3c69da