src/HOL/Real/real_arith.ML
changeset 21966 edab0ecfbd7c
parent 20254 58b71535ed00
child 22962 4bb05ba38939