src/HOL/RealDef.thy
changeset 51331 e7fab0b5dbe7
parent 51185 145d76c35f8b
child 51375 d9e62d9c98de
equal deleted inserted replaced
51330:f249bd08d851 51331:e7fab0b5dbe7