src/HOL/Real/Real.thy
changeset 21207 cef082634be9
parent 20505 1e223f64bd59
child 23454 c54975167be9
equal deleted inserted replaced
21206:2af4c7b3f7ef 21207:cef082634be9