src/HOL/Real/real_arith0.ML
changeset 13523 079af5c90d1c
parent 13462 56610e2ba220
child 13554 4679359bb218