src/HOL/Real/Real.thy
changeset 21966 edab0ecfbd7c
parent 20505 1e223f64bd59
child 23454 c54975167be9