src/HOL/Library/Extended_Real.thy
changeset 58669 6bade3d91c49
parent 58310 91ea607a34d8
child 58787 af9eb5e566dd
equal deleted inserted replaced
58668:1891f17c6124 58669:6bade3d91c49