src/HOL/Real.thy
changeset 56402 6d9a24f87460
parent 56217 dc429a5b13c4
child 56536 aefb4a8da31f