src/HOL/Real/RealAbs.ML
changeset 5126 01cbf154d926
parent 5078 7b5ea59c0275
child 5143 b94cd208f073