src/HOL/RealDef.thy
changeset 33566 1c62ac4ef6d1
parent 33209 d36ca3960e33
child 33657 a4179bf442d1
equal deleted inserted replaced
33300:939ca97f5a11 33566:1c62ac4ef6d1