src/HOL/Real/RealAbs.ML
changeset 8247 635339ef2dca
parent 7588 26384af93359
child 8838 4eaa99f0d223