src/HOL/Real/RealArith0.thy
changeset 14351 cd3ef10d02be
parent 14288 d149e3cbdb39