src/HOL/Real/RealDef.thy
changeset 21087 3e56528a39f7
parent 20554 c433e78d4203
child 21404 eb85850d3eb7