src/HOL/Real.thy
changeset 56524 f4ba736040fa
parent 56217 dc429a5b13c4
child 56536 aefb4a8da31f