src/HOL/Real/real_arith.ML
changeset 27090 2f45c1b1b05d
parent 24093 5d0ecd0c8f3c
child 27545 7165068bb61f