src/HOL/RealDef.thy
changeset 33556 cba22e2999d5
parent 33209 d36ca3960e33
child 33657 a4179bf442d1
equal deleted inserted replaced
33233:f9ff11344ec4 33556:cba22e2999d5