src/HOL/RealDef.thy
changeset 33519 e31a85f92ce9
parent 33209 d36ca3960e33
child 33657 a4179bf442d1
equal deleted inserted replaced
33518:24563731b9b2 33519:e31a85f92ce9