src/HOL/Real/real_arith.ML
changeset 20717 2244b0d719a0
parent 20254 58b71535ed00
child 22962 4bb05ba38939