src/HOL/Library/Extended_Real.thy
changeset 69689 ab5a8a2519b0
parent 69661 a03a63b81f44
child 69861 62e47f06d22c
equal deleted inserted replaced
69688:33843320448f 69689:ab5a8a2519b0