src/HOL/Real/RealDef.thy
changeset 7711 4dae7a4fceaf
parent 7219 4e3f386c2e37
child 9043 ca761fe227d8
equal deleted inserted replaced
7710:bf8cb3fc5d64 7711:4dae7a4fceaf