src/HOL/RealDef.thy
changeset 33254 d0c00b81db1d
parent 33209 d36ca3960e33
child 33657 a4179bf442d1