src/HOL/Hyperreal/HRealAbs.ML
changeset 14303 995212a00a50
parent 14299 0b5c0b0a3eba
child 14331 8dbbb7cf3637