src/HOL/Real.thy
changeset 56366 0362c3bb4d02
parent 56217 dc429a5b13c4
child 56536 aefb4a8da31f