src/HOL/Library/Extended_Real.thy
changeset 50986 c54ea7f5418f
parent 50819 5601ae592679
child 51000 c9adb50f74ad