src/HOL/Real.thy
changeset 60825 bacfb7c45d81
parent 60758 d8d85a8172b5
child 61070 b72a990adfe2