src/HOL/Real/Hyperreal/HRealAbs.thy
changeset 10662 cf6be1804912
parent 10045 c76b73e16711