src/HOL/Library/Extended_Real.thy
changeset 51085 d90218288d51
parent 50819 5601ae592679
child 51000 c9adb50f74ad