src/HOL/RealDef.thy
changeset 32728 2c55fc50f670
parent 32657 5f13912245ff
child 33197 de6285ebcc05