src/HOL/RealDef.thy
changeset 45775 6c340de26a0d
parent 45184 426dbd896c9e
child 45818 53a697f5454a
equal deleted inserted replaced
45774:9b11989f38b0 45775:6c340de26a0d