src/HOL/Real.thy
changeset 60864 20cfa048fe7c
parent 60758 d8d85a8172b5
child 61070 b72a990adfe2