src/HOL/Library/Extended_Real.thy
changeset 51073 a25b899a649d
parent 50819 5601ae592679
child 51000 c9adb50f74ad