src/HOL/Real.thy
changeset 62425 d0936b500bf5
parent 62398 a4b68bf18f8d
child 62623 dbc62f86a1a9
equal deleted inserted replaced
62424:8c47e7fcdb8d 62425:d0936b500bf5