src/HOL/Real/RealAbs.ML
changeset 8874 3242637f668c
parent 8838 4eaa99f0d223
child 9013 9dd0274f76af