src/HOL/Real/real_arith.ML
changeset 23024 70435ffe077d
parent 22970 b5910e3dec4c
child 23080 2f8d7aa1263b