src/HOL/Real.thy
changeset 56253 83b3c110f22d
parent 56217 dc429a5b13c4
child 56536 aefb4a8da31f