src/HOL/Real/RealAbs.ML
changeset 9408 d3d56e1d2ec1
parent 9065 15f82c9aa331
child 9432 8b7aad2abcc9