src/HOL/RealDef.thy
changeset 32728 2c55fc50f670
parent 32657 5f13912245ff
child 33197 de6285ebcc05
equal deleted inserted replaced
32727:9072201cd69d 32728:2c55fc50f670