src/HOL/Library/Extended_Real.thy
changeset 54446 31884c67d73a
parent 54416 7fb88ed6ff3c
child 54863 82acc20ded73