src/HOL/Real.thy
changeset 62069 28acb93a745f
parent 61944 5d06ecfdb472
child 62079 3a21fddf0328