src/HOL/Real.thy
changeset 56231 b98813774a63
parent 56217 dc429a5b13c4
child 56536 aefb4a8da31f