src/HOL/Real/RealAbs.ML
changeset 9502 50ec59aff389
parent 9432 8b7aad2abcc9
child 10043 a0364652e115