src/HOL/Real/Hyperreal/HRealAbs.thy
changeset 10673 337c00fd385b
parent 10045 c76b73e16711