src/HOL/Real.thy
changeset 58074 87a8cc594bf6
parent 58061 3d060f43accb
child 58097 cfd3cff9387b