src/HOL/RealDef.thy
changeset 48734 af91cd2301ba
parent 47902 34a9e81e5bfd
child 49962 a8cc904a6820
equal deleted inserted replaced
48733:18e76e2db6d4 48734:af91cd2301ba