src/HOL/RealDef.thy
changeset 48113 1c4500446ba4
parent 47902 34a9e81e5bfd
child 49962 a8cc904a6820
equal deleted inserted replaced
48112:b1240319ef15 48113:1c4500446ba4